rw [extIndep_iff_of_not_mem (by simp [heI, hne]), hI.insert_indep_iff_of_not_mem hxI, h.1] at hind
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
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 : x ∈ M.E \ M.cl (X \ {e})
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False