-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- If `χ` is a bad character, then `F` is an entire function. -/
private lemma F_differentiable (B : BadChar N) : Differentiable ℂ B.F

Proof state:
case h.inr
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
t : ℂ
ht : t ≠ 1
⊢ B.F t = (G * H) t

Tactic:
simp only [F, G, H, Function.update_of_ne ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]

Result:
no goals

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ DifferentiableAt ℂ B.F 1

Tactic:
refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt

Result:
case inr.refine_1
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z

case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ ContinuousAt B.F 1

Proof state:
case h.inl
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ B.F 1 = (G * H) 1

Tactic:
simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]

Result:
no goals

Proof state:
case inr.refine_2.hg
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt H 1

Tactic:
exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

Result:
no goals

Proof state:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt B.F 1

Tactic:
rw [this]

Result:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ B.F = G * H

Tactic:
ext1 t

Result:
case h
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
t : ℂ
⊢ B.F t = (G * H) t

Proof state:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ ContinuousAt B.F 1

Tactic:
let G := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1

Result:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
⊢ ContinuousAt B.F 1

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ Differentiable ℂ B.F

Tactic:
intro s

Result:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
⊢ DifferentiableAt ℂ B.F s

Proof state:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
⊢ ContinuousAt B.F 1

Tactic:
let H := Function.update (fun s ↦ (B.χ.LFunction s - B.χ.LFunction 1) / (s - 1)) 1
  (deriv B.χ.LFunction 1)

Result:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ ContinuousAt B.F 1

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
⊢ DifferentiableAt ℂ B.F s

Tactic:
rcases ne_or_eq s 1 with hs | rfl

Result:
case inl
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

case inr
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ DifferentiableAt ℂ B.F 1

Proof state:
case inl
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
exact B.F_differentiableAt_of_ne hs

Result:
no goals

Proof state:
case inr.refine_2.hf
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt G 1

Tactic:
simpa only [G, continuousAt_update_same] using riemannZeta_residue_one

Result:
no goals

Proof state:
case h
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
t : ℂ
⊢ B.F t = (G * H) t

Tactic:
rcases eq_or_ne t 1 with rfl | ht

Result:
case h.inl
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ B.F 1 = (G * H) 1

case h.inr
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
t : ℂ
ht : t ≠ 1
⊢ B.F t = (G * H) t

Proof state:
case h
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
t : ℂ
ht : t ∈ {1}ᶜ
⊢ DifferentiableAt ℂ B.F t

Tactic:
exact B.F_differentiableAt_of_ne ht

Result:
no goals

Proof state:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1

Tactic:
apply ContinuousAt.mul

Result:
case inr.refine_2.hf
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt G 1

case inr.refine_2.hg
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
G : ℂ → ℂ := Function.update (fun s => (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s => (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt H 1

Proof state:
case inr.refine_1
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z

Tactic:
filter_upwards [self_mem_nhdsWithin] with t ht

Result:
case h
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
t : ℂ
ht : t ∈ {1}ᶜ
⊢ DifferentiableAt ℂ B.F t