rw [maximal_extIndep_iff  hXE hind (insert_subset heX hJX)] at hcon
α : 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 \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
hcon : insert e J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ 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 \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
hcon :
  ¬(M.cl (insert e J \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ insert e J ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (insert e J \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ insert e J ∧ M.cl (X \ {e}) ∈ U)
⊢ False