exact fun h ↦ heF₀.2 (h.symm.subset (mem_cl_of_mem' _ (mem_insert _ _) heF₀.1))
case refine_2.intro.intro.refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ≠ M.cl (insert e F₀)
no goals