refine ⟨fun ⟨e, he, hYX⟩ ↦ ?_, fun ⟨e, he, _, heX, h_eq⟩ ↦ ⟨e, ⟨he, heX⟩, h_eq.symm⟩ ⟩
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)) ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
⊢ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y