∀ {κ : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : Finset α}
  {u : Finset κ} {f : γ → α → κ → β}, ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z