obtain (heI | heI) := em' (e ∈ I)
α : 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
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
case inl
α : 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
α : 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