exact hH.flat.cl_subset_of_subset hXH
case refine'_1.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
⊢ M.cl X ⊆ H
no goals