refine' subset_antisymm (subset_inter _ (M.cl_subset_ground _)) _
α : 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✝
⊢ M.cl X = ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X ⊆ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}

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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E ⊆ M.cl X