rw [extIndep_iff_of_not_mem heI] at hI
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False