rwa [inter_eq_self_of_subset_left hX] at hXH
α : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
H : Set α
hH : M.Hyperplane H
hXH : X ∩ M.E ⊆ H
⊢ X ⊆ H
no goals