exact ⟨H, hH, (M.subset_cl Y).trans hYH⟩
case refine'_1.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 : M.cl Y ≠ M.E
H : Set α
hH : M.Hyperplane H
hYH : M.cl Y ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H
no goals