no goals
G : Type u_3
G'✝ : Type ?u.536179
inst✝⁷ : Group G
inst✝⁶ : Group G'✝
A : Type ?u.536188
inst✝⁵ : AddGroup A
N : Type u_4
P : Type ?u.536197
inst✝⁴ : Group N
inst✝³ : Group P
K : Subgroup G
M : Type ?u.536214
inst✝² : MulOneClass M
G' : Type u_1
N' : Type u_2
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ ker (prodMap f g) = prod (ker f) (ker g)
rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]