rw [hyperplane_iff_covBy, covBy_iff, and_iff_right M.ground_flat,
  flat_iff_ssubset_cl_insert_forall h.1.1]
case refine'_2
α : 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 : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ M.Hyperplane H
case refine'_2
α : 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 : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ (∀ e ∈ M.E \ H, M.cl H ⊂ M.cl (insert e H)) ∧ H ⊂ M.E ∧ ∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E