simp_rw [or_iff_not_imp_left, ssubset_iff_subset_ne, and_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.Flat H →
    H ⊂ M.E →
      ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E) ↔ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E)
α : 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 H →
    H ⊆ M.E →
      H ≠ M.E →
        ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → ¬F = H → F = M.E) ↔
          ∀ (F : Set α), H ⊆ F → H ≠ F → M.Flat F → F = M.E)