exact ⟨e, he, h.cl_insert_eq he⟩
case intro
α : 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 : α
h : F₀ ⋖[M] F₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁
no goals