theorem Finset.prod_comm_3 {β : Type u_4} [CommMonoid β] {γ : Type u_1} {α : Type u_2} {δ : Type u_3} {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

Cyclically permute 3 nested instances of Finset.prod.

theorem Finset.sum_comm_3 {β : Type u_4} [AddCommMonoid β] {γ : Type u_1} {α : Type u_2} {δ : Type u_3} {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