rw [hJ.cl_eq_cl] at hI
case intro.intro.intro.inl
α : 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
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
hJ : M.Basis (I \ {e}) (X \ {e})
hIJ : I \ {e} ⊆ I \ {e}
hJX : I \ {e} ⊆ X
heJ : e ∉ I \ {e}
hJi : U.ExtIndep e (I \ {e})
⊢ False
case intro.intro.intro.inl
α : 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 (X \ {e}) ∉ U
hIX : I ⊆ X
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
hJ : M.Basis (I \ {e}) (X \ {e})
hIJ : I \ {e} ⊆ I \ {e}
hJX : I \ {e} ⊆ X
heJ : e ∉ I \ {e}
hJi : U.ExtIndep e (I \ {e})
⊢ False