obtain ⟨B₀, hB₀, hfk⟩ := hI
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : ∃ B, M✶.Base B ∧ B ⊆ M✶.E \ I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I