have h' : M.cl (X \ {e}) ∉ U ∧ e ∈ X := by
  simpa [maximal_extIndep_iff hXE hJi hJX, heJ, hJ.cl_eq_cl] using hcon J hIJ
α : 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 : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ 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}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ False
α : 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 : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ 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}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
h' : M.cl (X \ {e}) ∉ U ∧ e ∈ X
⊢ False