rw [hyperplane_iff_covBy, covBy_iff, and_iff_right M.ground_flat, and_congr_right_iff,
  and_congr_right_iff]
α : 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.Hyperplane H ↔ M.Flat H ∧ H ⊂ 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 →
      ((∀ (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)