rw [hI.diff_singleton_indep.mem_cl_iff', and_iff_right (hX' hx), mem_diff, and_iff_left hx.2,
  diff_singleton_eq_self heI]
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
⊢ x ∈ M.cl (I \ {e})
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
⊢ M.Indep (insert x I) → x ∈ I