rintro rfl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
⊢ x ≠ e
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
f : α
U✝ U : M.ModularCut
I : Set α
hIX : I ⊆ X
J : Set α
hJX : J ⊆ X
x : α
hJu : M.cl (J \ {x}) ∉ U
hXE : X ⊆ insert x M.E
hI : M.Indep (I \ {x}) ∧ M.cl (I \ {x}) ∉ U
hJ : M.Basis J (X \ {x})
hIJ : I \ {x} ⊆ J
heJ : x ∉ J
hJi : U.ExtIndep x J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep x K ∧ K ⊆ X}
heI : x ∈ I
hconJe : M.cl (X \ {x}) ∈ U
hssu : I \ {x} ⊂ J
hx : x ∈ J \ (I \ {x})
⊢ False