exact ⟨f, hf, hB₂.exchange_base_of_indep' hf.1 he.2 h₁,
  hB₁.exchange_base_of_indep' he.1 hf.2 h₂⟩
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})
no goals