rw [flat_iff_cl_self, contract_cl_eq, diff_union_self, ← M.cl_union_cl_right_eq,
  union_eq_self_of_subset_right (M.cl_subset_cl subset_union_right), cl_cl]
α : 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 : α
X C : Set α
⊢ (M ／ C).Flat (M.cl (X ∪ C) \ C)
no goals