rw [flat_iff_cl_self, contract_cl_eq, subset_antisymm_iff, subset_diff, diff_subset_iff,
  union_comm C, ← and_assoc, and_congr_left_iff, flat_iff_cl_self, subset_antisymm_iff,
  and_congr_right_iff]
α : 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ (M ／ C).Flat F ↔ M.Flat (F ∪ C) ∧ Disjoint F C
α : 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ Disjoint F C → M.cl (F ∪ C) ⊆ F ∪ C → (F ⊆ M.cl (F ∪ C) ↔ F ∪ C ⊆ M.cl (F ∪ C))