obtain ⟨I, hI⟩ := (C.extension e).exists_basis F (Fsub.trans (subset_insert _ _))
case refine'_1.inr.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C