rintro e ⟨heH, heE⟩
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
case refine'_2.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✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
⊢ e ∈ M.cl X