obtain ⟨f, hf, h₁, h₂⟩ := h1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
h1 : ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
f : α
hf : f ∈ B₂ \ B₁
h₁ : M.Indep (insert e B₂ \ {f})
h₂ : M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})