no goals
G : Type u_1
H : Type ?u.141455
A : Type ?u.141458
a a₁ a₂ b c : G
inst✝ : Group G
⊢ trivial G ⊆ Group.closure ∅
simp [Set.subset_def, (Group.closure.isSubgroup _).one_mem]
no goals
G : Type u_1
H : Type ?u.141455
A : Type ?u.141458
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∅ ⊆ trivial G
simp