awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
rwa : 1 < (↑s.re : EReal)
rwa₁ : (↑1 : EReal) < (↑s.re : EReal)
rwa₂ rwa₃ rwa₄ rwa₅ : 1 < s.re
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)

Tactic:
rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]

Premises used: DirichletCharacter.absicssaOfAbsConv_eq_one, EReal.coe_one, EReal.coe_lt_coe_iff
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)

Tactic:
have hs' : abscissaOfAbsConv ↗χ < s.re := by
    rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
⊢ LSeriesSummable
    (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
      (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
    s

Tactic:
have hΛ : LSeriesSummable (↗χ * ↗Λ) s := LSeriesSummable_twist_vonMangoldt χ hs
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
hΛ :
  LSeriesSummable
    (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
      (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
    s
inr :
  L (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦ Complex.log (↑n : ℂ)) s =
    L (logMul fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
⊢ L
      (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
      s =
    -deriv (L fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s /
      L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
rw [eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs, ← LSeries_convolution' hΛ hχ,
    convolution_twist_vonMangoldt, LSeries_deriv hs', neg_neg]

Premises used: LSeries_deriv, neg_neg, LSeries_convolution', DirichletCharacter.convolution_twist_vonMangoldt, DirichletCharacter.LSeries_ne_zero_of_one_lt_re, eq_div_iff
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
hΛ :
  LSeriesSummable
    (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
      (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
    s
n : ℕ
h : n ≠ 0
⊢ HMul.hMul (α := ℕ → ℂ) (β := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N))
      (fun (n : ℕ) ↦ Complex.log (↑n : ℂ)) n =
    logMul (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) n

Tactic:
simp [mul_comm, logMul]

Premises used: LSeries.logMul, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
hΛ :
  LSeriesSummable
    (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
      (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
    s
⊢ L (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦ Complex.log (↑n : ℂ)) s =
    L (logMul fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
exact LSeries_congr (fun _ ↦ by simp [mul_comm, logMul]) s

Premises used: LSeries_congr
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv (L 1) s / L 1 s

Tactic:
(LSeries_congr (fun {n} _ ↦ ?_) s).trans <|
    LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs

Premises used: LSeries_congr, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
refine :
  ∀ {n : ℕ},
    n ≠ 0 →
      (↑((Λ : (a : ℕ) → ℝ) n) : ℂ) =
        HMul.hMul (α := ℕ → ℂ) (β := ℕ → ℂ) (fun (n : ℕ) ↦ (1 : (a : ZMod 1) → ℂ) (↑n : ZMod 1))
          (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv (L 1) s / L 1 s

Tactic:
refine (LSeries_congr (fun {n} _ ↦ ?_) s).trans <|
    LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs

Premises used: LSeries_congr, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
h : n ≠ 0
⊢ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ) =
    HMul.hMul (α := ℕ → ℂ) (β := ℕ → ℂ) (fun (n : ℕ) ↦ (1 : (a : ZMod 1) → ℂ) (↑n : ZMod 1))
      (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n

Tactic:
simp [Subsingleton.eq_one (n : ZMod 1)]

Premises used: Subsingleton.eq_one, Nat.cast
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
rw : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / riemannZeta s
rw₁ : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / L 1 s
rw₂ rw₃ : -deriv riemannZeta s / L 1 s = -deriv riemannZeta s / L 1 s
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]

Premises used: LSeries_one_eq_riemannZeta, ArithmeticFunction.LSeries_vonMangoldt_eq
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
suffices : deriv (L 1) s = deriv riemannZeta s
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
suffices deriv (L 1) s = deriv riemannZeta s by
    rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ deriv (L 1) s = deriv riemannZeta s

Tactic:
Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_

Premises used: Iff.mpr, Filter.EventuallyEq.deriv_eq, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
refine : ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1
⊢ deriv (L 1) s = deriv riemannZeta s

Tactic:
refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_

Premises used: Iff.mpr, Filter.EventuallyEq.deriv_eq, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1

Tactic:
⟨{z | 1 < z.re}, (isOpen_lt continuous_const continuous_re).mem_nhds hs,
    fun _ ↦ LSeries_one_eq_riemannZeta⟩

Premises used: isOpen_lt, Complex.continuous_re, continuous_const, setOf, LSeries_one_eq_riemannZeta, Complex.re, And.intro, IsOpen.mem_nhds, LT.lt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1

Tactic:
exact ⟨{z | 1 < z.re}, (isOpen_lt continuous_const continuous_re).mem_nhds hs,
    fun _ ↦ LSeries_one_eq_riemannZeta⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
χ : DirichletCharacter ℂ 1
h : ∀ (x : ℂ), LFunction χ x = riemannZeta x
⊢ LFunction χ = riemannZeta

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
⊢ Eq (α := ZMod 1) 0 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
h : ZMod.LFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = riemannZeta x
h₁ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 0 : ℂ) (riemannZeta x) = riemannZeta x
h₂ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 1 : ℂ) (riemannZeta x) = riemannZeta x
h₃ : 1 * riemannZeta x = riemannZeta x
h₄ h₅ : riemannZeta x = riemannZeta x
⊢ LFunction χ x = riemannZeta x

Tactic:
rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]

Premises used: ZMod.LFunction_modOne_eq, DirichletCharacter.LFunction, map_one, one_mul
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LFunction χ s = LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s

Tactic:
ZMod.LFunction_eq_LSeries χ hs

Premises used: ZMod.LFunction_eq_LSeries, DirichletCharacter.LFunction, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ deriv (LFunction χ) s = deriv (LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s

Tactic:
Filter.EventuallyEq.deriv_eq ?_

Premises used: Filter.EventuallyEq.deriv_eq
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
refine : LFunction χ =ᶠ[𝓝 s] LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)
⊢ deriv (LFunction χ) s = deriv (LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s

Tactic:
refine Filter.EventuallyEq.deriv_eq ?_

Premises used: Filter.EventuallyEq.deriv_eq
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ {z : ℂ | 1 < z.re} ∈ 𝓝 s

Tactic:
have h : {z | 1 < z.re} ∈ nhds s :=
    (isOpen_lt continuous_const continuous_re).mem_nhds hs
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z : ℂ | 1 < z.re} ∈ 𝓝 s
h₁ : ∀ (z : ℂ) (hz : 1 < z.re), LFunction χ z = LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) z
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)

Tactic:
filter_upwards [h] with z hz
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z : ℂ | 1 < z.re} ∈ 𝓝 s
z : ℂ
hz : 1 < z.re
⊢ LFunction χ z = LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) z

Tactic:
LFunction_eq_LSeries χ hz

Premises used: DirichletCharacter.LFunction_eq_LSeries
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z : ℂ | 1 < z.re} ∈ 𝓝 s
z : ℂ
hz : 1 < z.re
⊢ LFunction χ z = LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) z

Tactic:
exact LFunction_eq_LSeries χ hz

Premises used: DirichletCharacter.LFunction_eq_LSeries
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : s ≠ 1 ∨ χ ≠ 1
⊢ DifferentiableAt ℂ (LFunction χ) s

Tactic:
ZMod.differentiableAt_LFunction χ s (hs.imp_right χ.sum_eq_zero_of_ne_one)

Premises used: ZMod.differentiableAt_LFunction, DirichletCharacter.LFunction, Or.imp_right, DFunLike.coe, MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
⊢ Differentiable ℂ (LFunction χ)

Tactic:
(differentiableAt_LFunction _ · <| Or.inr hχ)

Premises used: Differentiable, DirichletCharacter.differentiableAt_LFunction, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
⊢ LFunction χ (-(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) = 0

Tactic:
ZMod.LFunction_neg_two_mul_nat_add_one hχ.to_fun n

Premises used: DirichletCharacter.LFunction, ZMod.LFunction_neg_two_mul_nat_add_one, DirichletCharacter.Even.to_fun
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
inst_1 : NeZero n
obtain : ∀ (m : ℕ) [NeZero m.succ], LFunction χ (-HMul.hMul (α := ℂ) 2 (↑m.succ : ℂ)) = 0
⊢ LFunction χ (-HMul.hMul (α := ℂ) 2 (↑n : ℂ)) = 0

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
m : ℕ
inst_1 : NeZero m.succ
⊢ LFunction χ (-HMul.hMul (α := ℂ) 2 (↑m.succ : ℂ)) = 0

Tactic:
exact_mod_cast hχ.LFunction_neg_two_mul_nat_add_one m

Premises used: DirichletCharacter.Even.LFunction_neg_two_mul_nat_add_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Odd
n : ℕ
⊢ LFunction χ (-HMul.hMul (α := ℂ) 2 (↑n : ℂ) - 1) = 0

Tactic:
ZMod.LFunction_neg_two_mul_nat_sub_one hχ.to_fun n

Premises used: DirichletCharacter.Odd.to_fun, DirichletCharacter.LFunction, ZMod.LFunction_neg_two_mul_nat_sub_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
⊢ IsPreconnected (α := ℂ) {1}ᶜ

Tactic:
have hpc : IsPreconnected ({1}ᶜ : Set ℂ) :=
    (isConnected_compl_singleton_of_one_lt_rank (rank_real_complex ▸ Nat.one_lt_ofNat) _)
      |>.isPreconnected
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
⊢ Membership.mem (γ := Set ℂ) {1}ᶜ 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
⊢ Membership.mem (γ := Set ℂ) {1}ᶜ 2

Tactic:
have hne : 2 ∈ ({1}ᶜ : Set ℂ) := by simp
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (𝕜 := ℂ)
    (g := fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))) ?_ ?_ hpc hne ?_ hs

Premises used: AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
refine_1 :
  AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ))
    {1}ᶜ
refine_2 :
  AnalyticOnNhd ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ
refine_3 :
  LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) =ᶠ[𝓝 2] fun (s : ℂ) ↦
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
refine AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (𝕜 := ℂ)
    (g := fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))) ?_ ?_ hpc hne ?_ hs

Premises used: AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ))
    {1}ᶜ

Tactic:
DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton

Premises used: isOpen_compl_singleton, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
refine_1 :
  ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {1}ᶜ s),
    DifferentiableWithinAt ℂ
      (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ)) {1}ᶜ s
⊢ AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ))
    {1}ᶜ

Tactic:
refine DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton

Premises used: isOpen_compl_singleton, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
⊢ DifferentiableWithinAt ℂ
    (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ)) {1}ᶜ s

Tactic:
(differentiableAt_LFunction _ _ (.inl hs)).differentiableWithinAt

Premises used: DirichletCharacter.differentiableAt_LFunction, DifferentiableAt.differentiableWithinAt, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
⊢ DifferentiableWithinAt ℂ
    (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ)) {1}ᶜ s

Tactic:
exact (differentiableAt_LFunction _ _ (.inl hs)).differentiableWithinAt

Premises used: DirichletCharacter.differentiableAt_LFunction, DifferentiableAt.differentiableWithinAt, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ AnalyticOnNhd ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ

Tactic:
DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton

Premises used: isOpen_compl_singleton, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
refine_2 :
  ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {1}ᶜ s),
    DifferentiableWithinAt ℂ (F := ℂ)
      (fun (s : ℂ) ↦
        LFunction χ s *
          ∏ p ∈ N.primeFactors,
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
      {1}ᶜ s
⊢ AnalyticOnNhd ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ

Tactic:
refine DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton

Premises used: isOpen_compl_singleton, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
⊢ DifferentiableWithinAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ s

Tactic:
((differentiableAt_LFunction _ _ (.inl hs)).mul ?_).differentiableWithinAt

Premises used: DifferentiableAt.mul, DirichletCharacter.differentiableAt_LFunction, DifferentiableAt.differentiableWithinAt, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
refine_2 :
  DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    s
⊢ DifferentiableWithinAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ s

Tactic:
refine ((differentiableAt_LFunction _ _ (.inl hs)).mul ?_).differentiableWithinAt

Premises used: DifferentiableAt.mul, DirichletCharacter.differentiableAt_LFunction, DifferentiableAt.differentiableWithinAt, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    s

Tactic:
.fun_finsetProd fun i h ↦ ?_

Premises used: DifferentiableAt.fun_finsetProd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
refine_2 :
  ∀ (i : ℕ) (h : i ∈ N.primeFactors),
    DifferentiableAt ℂ (F := ℂ)
      (fun (s : ℂ) ↦
        1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑i : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑i : ℂ) (-s)))
      s
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    s

Tactic:
refine .fun_finsetProd fun i h ↦ ?_
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
i : ℕ
h : i ∈ N.primeFactors
⊢ NeZero i

Tactic:
have : NeZero i := ⟨(Nat.pos_of_mem_primeFactors h).ne'⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s_1 : ℂ
hs_1 : s_1 ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
i : ℕ
h : i ∈ N.primeFactors
this : NeZero i
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑i : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑i : ℂ) (-s)))
    s

Tactic:
fun_prop