have hJ'X : J' ⊆ X := insert_subset (hIX heI) (diff_subset.trans hJX)
case intro.intro.intro.inr
α : 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
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
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
⊢ False
case intro.intro.intro.inr
α : 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
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
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
⊢ False