obtain ⟨I, hI⟩ := M.exists_basis (C ∩ M.E)
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C : Set α
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D