rw [Point, flat_contract_iff, covBy_iff_relRank_eq_one, relRank_cl_left,
  union_comm C, ← relRank_eq_relRank_union, and_iff_right (cl_flat _ _),
  ← relRank_eq_er_contract, and_assoc, and_assoc, and_congr_right_iff, and_comm,
  and_congr_left_iff, iff_and_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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ (M ／ C).Point P ↔ (M.cl C ⋖[M] (C ∪ P)) ∧ Disjoint P 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✝
⊢ M.Flat (P ∪ C) → Disjoint P C → M.relRank C P = 1 → M.cl C ⊆ P ∪ C