simp only [Ico_succ_right, reduceSucc, Nat.div_zero, smul_zero, map_zero, zero_add] at this
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = (N / 0) • f 0 + ∑ x ∈ Ico (succ 0) (N + 1), (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ x ∈ Icc 1 N, (f * ↑ζ) x = ∑ x ∈ Icc 1 N, (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1