rw [←not_indep_iff, (C.extension_indep e), not_or, not_indep_iff _] at x_dep
case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ insert e (M.cl I)
case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : M.Dep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ insert e (M.cl I)

α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ insert x I ⊆ M.E