rintro ⟨H, hH, hYH⟩ hY
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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ H, M.Hyperplane H ∧ Y ⊆ H) → M.cl Y ≠ M.E
case refine'_2.intro.intro
α : 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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ False