obtain ⟨I, rfl, heI'⟩ : ∃ J, I = insert e J ∧ e ∉ J := ⟨I \ {e}, by simp [heI], by simp⟩
case inr
α : 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 α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
case inr.intro.intro
α : 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
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)