rw [covBy_iff, and_iff_right hF₀, and_iff_right hF₁]
α : 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₀
hF₁ : M.Flat F₁
⊢ F₀ ⋖[M] F₁ ↔ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
no goals