simpa [extIndep_iff_of_mem heI, heI']
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
this : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)
no goals