exact (M.cl_subset_ground _).antisymm ((hH.cl_insert_eq heH (hX' heX)).symm.trans_subset
  (M.cl_subset_cl (insert_subset heX hX.subset)))
case 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 : α
hH : M.Hyperplane H
hX : H ⊂ X
hX' : autoParam (X ⊆ M.E) _auto✝
e : α
heX : e ∈ X
heH : e ∉ H
⊢ M.cl X = M.E
no goals