rw [base_restrict_iff] at h₁ 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 α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : (M ↾ X).Base (insert e I₂ \ {f})
h₂ : (M ↾ X).Base (insert f I₁ \ {e})
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
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 α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : M.Basis (insert e I₂ \ {f}) X
h₂ : M.Basis (insert f I₁ \ {e}) X
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X