rw [ex_basis.indep.mem_cl_iff, or_iff_left xnI, dep_iff,
 C.extension_ground, insert_subset_insert_iff xnI, (C.extension_indep x), not_or,
 and_iff_left (hI.indep.subset_ground)]
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
⊢ x ∈ (C.extension x).cl I
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
⊢ ¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)