exact by_contra fun hne ↦ hX' (h.spanning_of_ssuperset (hHX.ssubset_of_ne hne))
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
no goals