exact hI.1.2.subset subset_union_left
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R✝ B X Y Z K C C₁ C₂ J R : Set α
hI : (Disjoint I J ∧ M.Indep (I ∪ J)) ∧ Disjoint I R
hJ : M.Basis J (C ∩ M.E)
hM : M ／ C = M ／ J ＼ R
⊢ M.Indep I
no goals