exact mem_of_mem_of_subset (hF₀.cl_exchange ⟨hFF₁ hfF, hfF₀⟩).1
  (hF.cl_subset_of_subset (insert_subset hfF hF₀F))
case refine_2.intro.intro.refine_3.intro.intro
α : 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 : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
hss : F₀ ⊂ F
f : α
hfF : f ∈ F
hfF₀ : f ∉ F₀
⊢ e ∈ F
no goals