-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- `B.F` agrees with the L-series of `zetaMul χ` on `1 < s.re`. -/
private lemma F_eq_LSeries (B : BadChar N) {s : ℂ} (hs : 1 < s.re) :
    B.F s = LSeries B.χ.zetaMul s

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
h : s = 1
⊢ False

Tactic:
simp only [h, one_re, lt_self_iff_false] at hs

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ B.F s = LSeries (⇑B.χ.zetaMul) s

Tactic:
rw [F, zetaMul, ← coe_mul, LSeries_convolution']

Result:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s => riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑ζ) s * LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

case hf
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑↑ζ) s

case hg
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s => riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑ζ) s * LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Tactic:
have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs

Result:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ Function.update (fun s => riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑ζ) s * LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Proof state:
case hg
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Tactic:
exact (LSeriesSummable_congr _ fun h ↦ (B.χ.apply_eq_toArithmeticFunction_apply h).symm).mpr <|
  ZMod.LSeriesSummable_of_one_lt_re B.χ hs

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ Function.update (fun s => riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑ζ) s * LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Tactic:
simp only [ne_eq, hs', not_false_eq_true, Function.update_of_ne, B.χ.LFunction_eq_LSeries hs]

Result:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s * LSeries (fun x => B.χ ↑x) s = LSeries (⇑↑ζ) s * LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s * LSeries (fun x => B.χ ↑x) s = LSeries (⇑↑ζ) s * LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Tactic:
congr 1

Result:
case e_a
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s = LSeries (⇑↑ζ) s

case e_a
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun x => B.χ ↑x) s = LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun x => B.χ ↑x) s = LSeries (⇑(toArithmeticFunction fun x => B.χ ↑x)) s

Tactic:
exact LSeries_congr s B.χ.apply_eq_toArithmeticFunction_apply

Result:
no goals

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s = LSeries (⇑↑ζ) s

Tactic:
simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]

Result:
no goals

Proof state:
case hf
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑↑ζ) s

Tactic:
exact LSeriesSummable_zeta_iff.mpr hs

Result:
no goals