simp only [hF₀, wCovBy_self, or_self, true_iff]
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀ ∨ F = F₀
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ hF₁ : M.Flat F₀
⊢ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀