exact not_mem_of_mem_diff_cl (h_eq ▸ hind.1) <| by simp [hi, hxe]
case pos.inl.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ False
no goals