∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_8} [inst_2 : FunLike F M Nᵐᵒᵖ]
  [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M),
  MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod