no goals
G : Type u_1
G' : Type ?u.445572
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.445581
inst✝ : AddGroup A
s✝ s : Set G
⊢ closure s ≤ normalClosure s
simp only [subset_normalClosure, closure_le]