rintro rfl
α : 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
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
⊢ x ≠ e
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
f : α
U : M.ModularCut
hIX : I ⊆ X
x : α
hxI : x ∉ I
hi : x ∈ X
hX : X ⊆ insert x M.E
hI : U.ExtIndep x I
hss : I \ {x} ⊆ X \ {x}
hX' : X \ {x} ⊆ M.E
h :
  M.cl (I \ {x}) = M.cl (X \ {x}) ∧ (x ∈ X → ¬(x ∈ I ↔ M.cl (X \ {x}) ∈ U)) ∨
    (M.cl (I \ {x}) ⋖[M] M.cl (X \ {x})) ∧ x ∈ I ∧ M.cl (X \ {x}) ∈ U
hind : U.ExtIndep x (insert x I)
heI : x ∈ I
⊢ False