refine' ⟨fun h ↦ ⟨⟨h.subset_ground, h.not_spanning⟩, fun X hX hX' hHX ↦ _⟩, fun h ↦ _⟩
α : 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 ↔ (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
case refine'_1
α : 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 : M.Hyperplane H
X : Set α
hX : X ⊆ M.E
hX' : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X

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