-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The L function of the trivial Dirichlet character mod `N` has a simple pole with
residue `∏ p ∈ N.primeFactors, (1 - p⁻¹)` at `s = 1`. -/
lemma LFunctionTrivChar_residue_one :
    Tendsto (fun s ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1)
      (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹))

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
rw [tendsto_congr' H]

Result:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
conv => enter [3, 1]; rw [← mul_one <| Finset.prod ..]; enter [1, 2, p]; rw [← cpow_neg_one]

Result:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 ((∏ p ∈ N.primeFactors, (1 - ↑p ^ (-1))) * 1))

Proof state:
N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun s => (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
have H : (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1]
      fun s ↦ (∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))) * ((s - 1) * riemannZeta s) := by
  refine Set.EqOn.eventuallyEq_nhdsWithin fun s hs ↦ ?_
  rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]

Result:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Proof state:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ∈ {1}ᶜ
⊢ (s - 1) * LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)

Tactic:
rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 ((∏ p ∈ N.primeFactors, (1 - ↑p ^ (-1))) * 1))

Tactic:
refine .mul (f := fun s ↦ ∏ p ∈ N.primeFactors, _) ?_ riemannZeta_residue_one

Result:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-1))))

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Continuous fun s => ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))

Tactic:
exact continuous_finset_prod _ fun p hp ↦ by
  have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
  fun_prop

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous fun s => 1 - ↑p ^ (-s)

Tactic:
fun_prop

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s => ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-1))))

Tactic:
refine tendsto_nhdsWithin_of_tendsto_nhds <| Continuous.tendsto ?_ 1

Result:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Continuous fun s => ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))

Proof state:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s => 1 - ↑p ^ (-s)

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩

Result:
N : ℕ
inst✝ : NeZero N
H :
  (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous fun s => 1 - ↑p ^ (-s)

Proof state:
N : ℕ
inst✝ : NeZero N
⊢ (fun s => (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s =>
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)

Tactic:
refine Set.EqOn.eventuallyEq_nhdsWithin fun s hs ↦ ?_

Result:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ∈ {1}ᶜ
⊢ (s - 1) * LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)