rw [hF₀.cl_insert_eq_cl_insert_of_mem ⟨heX, he.2⟩]
case h.refine'_2
α : 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✝ : α
hF₀ : M.Flat F₀
he : e ∈ M.E \ F₀
f : α
a✝ : f ∈ M.E \ F₀
heX : e ∈ M.cl (insert f F₀)
⊢ M.cl (insert f F₀) = M.cl (insert e F₀)
no goals