refine' ⟨subset_inter_iff.2 ⟨sub_inter.1, sub_inter.2.trans (subset_insert _ _)⟩,
 fun J J_ind I_sub_J J_sub_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
heX : e ∉ X
I : Set α
hI : M.Basis' I X
sub_inter : I ⊆ X ∧ I ⊆ M.E
⊢ I ⊆ X ∩ insert e M.E ∧ ∀ (J : Set α), (C.extension e).Indep J → I ⊆ J → J ⊆ X ∩ insert e M.E → I = J
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
heX : e ∉ X
I : Set α
hI : M.Basis' I X
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
⊢ I = J