suffices h1 : (∃ f, f ∈ B₂ \ B₁ ∧  M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})) by
  obtain ⟨f, hf, h₁, h₂⟩ := h1;
  exact ⟨f, hf, hB₂.exchange_base_of_indep' hf.1 he.2 h₁,
    hB₁.exchange_base_of_indep' he.1 hf.2 h₂⟩
α : 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 ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
α : 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 ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})