∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun Commute f)) (y : β),
  (∀ x ∈ s, Commute y (f x)) → Commute y (s.noncommProd f comm)