Theorem: Finset.sum_shift_front (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ cumsum u (n + 1) = u 0 + cumsum (shift u) n
Tactic:
simp_rw [add_comm n, cumsum, sum_range_add, sum_range_one, add_comm 1]
State after:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ u 0 + ∑ x ∈ range n, u (x + 1) = u 0 + ∑ i ∈ range n, shift u i

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ u 0 + ∑ x ∈ range n, u (x + 1) = u 0 + ∑ i ∈ range n, shift u i
Tactic:
rfl
State after:
no goals