simp_rw [CovBy, covBy_iff_lt_and_eq_or_eq]
α : 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 : α
⊢ F₀ ⋖[M] F₁ ↔ M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
α : 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 : α
⊢ (∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
      ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf) ↔
    M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁