no goals
ι : Type u_1
α : Type ?u.46129
M : Type u_3
N : Type u_4
P : Type ?u.46138
M₀ : Type ?u.46141
G✝ : Type ?u.46144
R : Type ?u.46147
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
L : List ι
f : ι → M
G : Type u_2
inst✝ : MonoidHomClass G M N
g : G
⊢ prod (map (↑g ∘ f) L) = ↑g (prod (map f L))
rw [← prod_hom, map_map]