rw [basis'_iff_basis_inter_ground, C.extension_ground, basis_iff, C.extension_indep,
and_iff_right (Or.inl hI.indep)]
case ex_basis
α : 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
⊢ (C.extension e).Basis' I X
case ex_basis
α : 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
⊢ I ⊆ X ∩ insert e M.E ∧ ∀ (J : Set α), (C.extension e).Indep J → I ⊆ J → J ⊆ X ∩ insert e M.E → I = J