simp only [covBy_iff_relRank_eq_one, cl_flat, relRank_cl_left, relRank_empty_left, true_and,
  and_congr_right_iff, and_iff_right_iff_imp]
α : 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 : α
⊢ M.cl ∅ ⋖[M] P ↔ M.Point P
α : 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 : α
⊢ M.Flat P → M.er P = 1 → M.cl ∅ ⊆ P