no goals
ι : Type ?u.30337
α : Type ?u.30340
M : Type u_2
N : Type u_3
P : Type ?u.30349
M₀ : Type ?u.30352
G : Type ?u.30355
R : Type ?u.30358
inst✝² : Monoid M
inst✝¹ : Monoid N
F : Type u_1
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ unop (↑f (prod l)) = prod (reverse (map (unop ∘ ↑f) l))
rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]