Theorem: Sum3Cycle (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommMonoid M
s : Finset α
t : Finset β
u : Finset γ
f : α → β → γ → M
⊢ ∑ a ∈ s, ∑ b ∈ t, ∑ c ∈ u, f a b c = ∑ b ∈ t, ∑ c ∈ u, ∑ a ∈ s, f a b c
Tactic:
rw [sum_comm]
State after:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommMonoid M
s : Finset α
t : Finset β
u : Finset γ
f : α → β → γ → M
⊢ ∑ y ∈ t, ∑ x ∈ s, ∑ c ∈ u, f x y c = ∑ b ∈ t, ∑ c ∈ u, ∑ a ∈ s, f a b c

State before:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommMonoid M
s : Finset α
t : Finset β
u : Finset γ
f : α → β → γ → M
⊢ ∑ y ∈ t, ∑ x ∈ s, ∑ c ∈ u, f x y c = ∑ b ∈ t, ∑ c ∈ u, ∑ a ∈ s, f a b c
Tactic:
simp_rw [@sum_comm _ _ γ]
State after:
no goals