Theorem: Matroid.Hyperplane.cl_insert_eq_univ (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
he : e ∈ M.E \ H
⊢ M.cl (insert e H) = M.E
Tactic:
refine' hH.ssuperset_eq_univ_of_flat (M.cl_flat _)
  ((ssubset_insert he.2).trans_subset (M.subset_cl _ _))
State after:
α : 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
he : e ∈ M.E \ H
⊢ insert e H ⊆ M.E

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
he : e ∈ M.E \ H
⊢ insert e H ⊆ M.E
Tactic:
rw [insert_eq, union_subset_iff, singleton_subset_iff]
State after:
α : 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
he : e ∈ M.E \ H
⊢ e ∈ M.E ∧ H ⊆ M.E

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
he : e ∈ M.E \ H
⊢ e ∈ M.E ∧ H ⊆ M.E
Tactic:
exact ⟨he.1, hH.subset_ground⟩
State after:
no goals