no goals
α : Type ?u.32325
G : Type u_1
A : Type ?u.32331
S : Type ?u.32334
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
N H : Subgroup G
inst✝ : Normal N
⊢ ↑(N ⊔ H) = ↑N * ↑H
rw [← set_mul_normal_comm, sup_comm, mul_normal]