exact fun _ _ _  ↦
  ⟨fun h F hHF hne' hF ↦ h F hF hHF hF.subset_ground hne'.symm, fun h F hF hHF _ hne' ↦
    h F hHF (Ne.symm hne') 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 : α
⊢ 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)
no goals