Theorem: Matroid.Hyperplane.cl_eq_ground_of_ssuperset (Matroid/Flat.lean)

State before:
α : 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✝
⊢ M.cl X = M.E
Tactic:
obtain ⟨e, heX, heH⟩ := exists_of_ssubset hX
State after:
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

State before:
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
Tactic:
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)))
State after:
no goals