no goals
G : Type u_1
G' : Type ?u.302242
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.302251
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.302278
inst✝ : Group P
⊢ ↑(prod ⊥ ⊥) = ↑⊥
simp [coe_prod, Prod.one_eq_mk]