no goals
ι : Type ?u.28940
α : Type ?u.28943
M : Type u_1
N : Type ?u.28949
P : Type ?u.28952
M₀ : Type ?u.28955
G : Type ?u.28958
R : Type ?u.28961
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop (prod l) = prod (reverse (map unop l))
rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
  op_comp_unop, map_id]