have hI := h.indep.subset subset_union_right
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
⊢ (M ／ I).Basis J X
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ (M ／ I).Basis J X