obtain ⟨-, heI⟩ := show I ⊆ M.E ∧ e ∉ I by simpa [subset_diff] using hI
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
heI : e ∉ I
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I