rwa [hI.insert_indep_iff_of_not_mem heI.2, hI'.flat.cl]
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hf : ¬M.Coloop f
⊢ M.Indep (insert e I)
no goals