no goals
G : Type u_1
G' : Type ?u.220679
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.220688
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
⊢ closure {1} = ⊥
simp [eq_bot_iff_forall, mem_closure_singleton]