rw [← union_eq_self_of_subset_right (M.cl_subset_cl (subset_insert e F)),
  ← union_eq_self_of_subset_right (M.cl_subset_cl (subset_insert f F)), hF.cl,
  ← diff_union_self, h, diff_union_self]
α : 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
e f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) \ F = M.cl (insert f F) \ F
⊢ M.cl (insert e F) = M.cl (insert f F)
no goals