no goals
F : Type u_1
ι : Type ?u.159885
α : Type u_4
β : Type u_2
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : MonoidHomClass F β γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
g : F
⊢ ↑g (noncommProd s f comm) =
    noncommProd s (fun i => ↑g (f i))
      (_ : ∀ (x : α), x ∈ ↑s → ∀ (y : α), y ∈ ↑s → x ≠ y → Commute (↑g (f x)) (↑g (f y)))
simp [noncommProd, Multiset.noncommProd_map]