-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- The L-function of `Φ` has a residue at `s = 1` equal to the average value of `Φ`. -/
lemma LFunction_residue_one (Φ : ZMod N → ℂ) :
    Tendsto (fun s ↦ (s - 1) * LFunction Φ s) (𝓝[≠] 1) (𝓝 (∑ j, Φ j / N))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (fun s => (s - 1) * LFunction Φ s) (𝓝[≠] 1) (𝓝 (∑ j : ZMod N, Φ j / ↑N))

Tactic:
simp only [sum_div, LFunction, mul_sum]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (fun s => ∑ i : ZMod N, (s - 1) * (↑N ^ (-s) * (Φ i * hurwitzZeta (toAddCircle i) s))) (𝓝[≠] 1)
    (𝓝 (∑ j : ZMod N, Φ j / ↑N))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ ∀ (a b c d : ℂ), a * (b * (c * d)) = c * (b * (a * d))

Tactic:
intros

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
a✝ b✝ c✝ d✝ : ℂ
⊢ a✝ * (b✝ * (c✝ * d✝)) = c✝ * (b✝ * (a✝ * d✝))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
a✝ b✝ c✝ d✝ : ℂ
⊢ a✝ * (b✝ * (c✝ * d✝)) = c✝ * (b✝ * (a✝ * d✝))

Tactic:
ring

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j / ↑N))

Tactic:
rw [(by ring : Φ j / N = Φ j * (1 / N * 1)), one_div, ← cpow_neg_one]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (↑N ^ (-1) * 1)))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Φ j / ↑N = Φ j * (1 / ↑N * 1)

Tactic:
ring

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => Φ j * (↑N ^ (-s) * ((s - 1) * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (↑N ^ (-1) * 1)))

Tactic:
refine tendsto_const_nhds.mul (.mul ?_ <| hurwitzZeta_residue_one _)

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => ↑N ^ (-s)) (𝓝[≠] 1) (𝓝 (↑N ^ (-1)))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => ↑N ^ (-s)) (𝓝[≠] 1) (𝓝 (↑N ^ (-1)))

Tactic:
exact ((continuous_neg.const_cpow (Or.inl <| NeZero.ne _)).tendsto _).mono_left
  nhdsWithin_le_nhds

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (↑N ^ (-1) * 1)))

Tactic:
simp only [show ∀ a b c d : ℂ, a * (b * (c * d)) = c * (b * (a * d)) by intros; ring]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => Φ j * (↑N ^ (-s) * ((s - 1) * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (↑N ^ (-1) * 1)))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (fun s => ∑ i : ZMod N, (s - 1) * (↑N ^ (-s) * (Φ i * hurwitzZeta (toAddCircle i) s))) (𝓝[≠] 1)
    (𝓝 (∑ j : ZMod N, Φ j / ↑N))

Tactic:
refine tendsto_finset_sum _ fun j _ ↦ ?_

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s => (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j / ↑N))