simp [show e ∉ I from fun heI ↦ by simpa using hI heI]
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
I : Set α
hI : I ⊆ (C.extension e ＼ e).E
⊢ (C.extension e ＼ e).Indep I ↔ M.Indep I
no goals