awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) χ) =ᶠ[𝓝 2] fun (s : ℂ) ↦
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
eventually_of_mem ?_ (fun t (ht : 1 < t.re) ↦ ?_)

Premises used: Filter.EventuallyEq, Filter.eventually_of_mem
-- 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_3 : Membership.mem (γ := Filter ℂ) (𝓝 2) fun (t : ℂ) ↦ Real.lt✝ 1 t.re
refine_3₁ :
  ∀ (t : ℂ) (ht : 1 < t.re),
    LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) t =
      (fun (s : ℂ) ↦
          LFunction χ s *
            ∏ p ∈ N.primeFactors,
              (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
        t
⊢ 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)))

Tactic:
refine eventually_of_mem ?_ (fun t (ht : 1 < t.re) ↦ ?_)

Premises used: Filter.eventually_of_mem
-- 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
⊢ 1 < re 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}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ Membership.mem (γ := Filter ℂ) (𝓝 2) fun (t : ℂ) ↦ Real.lt✝ 1 t.re

Tactic:
exact (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp : 1 < (2 : ℂ).re)

Premises used: Complex.continuous_re, isOpen_Ioi, IsOpen.mem_nhds, Continuous.isOpen_preimage
-- 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
t : ℂ
ht : 1 < t.re
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) t =
    (fun (s : ℂ) ↦
        LFunction χ s *
          ∏ p ∈ N.primeFactors,
            (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
      t

Tactic:
simpa [LFunction_eq_LSeries _ ht] using LSeries_changeLevel hMN χ ht

Premises used: DirichletCharacter.LFunction_eq_LSeries, DirichletCharacter.LSeries_changeLevel
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1 ∨ s ≠ 1
inl :
  ∀ (h : χ ≠ 1),
    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)))
inr :
  ∀ (h : s ≠ 1),
    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)))
⊢ 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:
rcases h with h | h
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
⊢ Ne (α := DirichletCharacter ℂ N)
    ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N)
    (1 : DirichletCharacter ℂ N)

Tactic:
have hχ : changeLevel hMN χ ≠ 1 := h ∘ (changeLevel_eq_one_iff hMN).mp
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ :
  Ne (α := DirichletCharacter ℂ N)
    ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N)
    (1 : DirichletCharacter ℂ N)
p : ℕ
hp : p ∈ N.primeFactors
⊢ NeZero p

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ :
  Ne (α := DirichletCharacter ℂ N)
    ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N)
    (1 : DirichletCharacter ℂ N)
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦
    1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ :
  Ne (α := DirichletCharacter ℂ N)
    ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N)
    (1 : DirichletCharacter ℂ N)
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
have h' : Continuous fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * ↑p ^ (-s)) :=
      (differentiable_LFunction h).continuous.mul <| continuous_finsetProd _ fun p hp ↦ by
        have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
        fun_prop
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ :
  Ne (α := DirichletCharacter ℂ N)
    ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N)
    (1 : DirichletCharacter ℂ N)
h' :
  Continuous (Y := ℂ) 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:
congrFun ((differentiable_LFunction hχ).continuous.ext_on
      (dense_compl_singleton 1) h' (fun _ h ↦ LFunction_changeLevel_aux hMN χ h)) s

Premises used: DirichletCharacter.differentiable_LFunction, Continuous.ext_on, congrFun, dense_compl_singleton, OfNat.ofNat, Differentiable.continuous, _private.0.DirichletCharacter.LFunction_changeLevel_aux
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ :
  Ne (α := DirichletCharacter ℂ N)
    ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N)
    (1 : DirichletCharacter ℂ N)
h' :
  Continuous (Y := ℂ) 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:
exact congrFun ((differentiable_LFunction hχ).continuous.ext_on
      (dense_compl_singleton 1) h' (fun _ h ↦ LFunction_changeLevel_aux hMN χ h)) s

Premises used: DirichletCharacter.differentiable_LFunction, Continuous.ext_on, congrFun, dense_compl_singleton, OfNat.ofNat, Differentiable.continuous, _private.0.DirichletCharacter.LFunction_changeLevel_aux
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : s ≠ 1
⊢ 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:
LFunction_changeLevel_aux hMN χ h

Premises used: _private.0.DirichletCharacter.LFunction_changeLevel_aux
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : s ≠ 1
⊢ 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:
exact LFunction_changeLevel_aux hMN χ h

Premises used: _private.0.DirichletCharacter.LFunction_changeLevel_aux
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : s ≠ 1
rw :
  LFunction (N := N) ((changeLevel ⋯ : (a : DirichletCharacter ℂ 1) → DirichletCharacter ℂ N) 1) s =
    LFunction (N := 1) 1 s * ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
⊢ LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * riemannZeta s

Tactic:
rw [← LFunction_modOne_eq (χ := 1), LFunctionTrivChar, ← changeLevel_one N.one_dvd, mul_comm]

Premises used: DirichletCharacter.LFunction_modOne_eq, DirichletCharacter.changeLevel_one, mul_comm, Nat.one_dvd, DirichletCharacter.LFunctionTrivChar
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunction (N := N) ((changeLevel ⋯ : (a : DirichletCharacter ℂ 1) → DirichletCharacter ℂ N) 1) s =
    LFunction (N := 1) 1 s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑p : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
LFunction_changeLevel N.one_dvd 1 (.inr hs)

Premises used: DirichletCharacter.LFunction_changeLevel, Nat.one_dvd, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : s ≠ 1
h :
  ∀ p ∈ N.primeFactors,
    HPow.hPow (α := ℂ) (↑p : ℂ) (-s) =
      HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑p : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
⊢ LFunction (N := N) ((changeLevel ⋯ : (a : DirichletCharacter ℂ 1) → DirichletCharacter ℂ N) 1) s =
    LFunction (N := 1) 1 s * ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))

Tactic:
convert! LFunction_changeLevel N.one_dvd 1 (.inr hs) using 4 with p

Premises used: DirichletCharacter.LFunction_changeLevel, Nat.one_dvd, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
h_1 : p ∈ N.primeFactors
h : HPow.hPow (α := ℂ) (↑p : ℂ) (-s) = 1 * HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
h₁ h₂ : HPow.hPow (α := ℂ) (↑p : ℂ) (-s) = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
⊢ HPow.hPow (α := ℂ) (↑p : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑p : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))

Tactic:
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]

Premises used: MulChar.one_apply, isUnit_of_subsingleton, one_mul
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)

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

Premises used: Set.EqOn.eventuallyEq_nhdsWithin
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
refine :
  ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {1}ᶜ s),
    (s - 1) * LFunctionTrivChar N s =
      (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)

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

Premises used: Set.EqOn.eventuallyEq_nhdsWithin
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
rw :
  (s - 1) * LFunctionTrivChar N s =
    (s - 1) * ((∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * riemannZeta s)
rw₁ rw₂ :
  (s - 1) * ((∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * riemannZeta s) =
    (s - 1) * ((∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * riemannZeta s)
⊢ (s - 1) * LFunctionTrivChar N s =
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)

Tactic:
rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]

Premises used: DirichletCharacter.LFunctionTrivChar_eq_mul_riemannZeta, mul_left_comm
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)

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]
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
rw :
  Tendsto (β := ℂ)
    (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

Tactic:
rw [tendsto_congr' H]

Premises used: Filter.tendsto_congr'
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
enter : ∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹
| Tendsto (β := ℂ)
    (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

Tactic:
enter [3, 1]
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
rw : HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 1
| ∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹

Tactic:
rw [← mul_one <| Finset.prod ..]

Premises used: Finset.prod, mul_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
h : ∀ (p : ℕ), HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹
| HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 1

Tactic:
enter [1, 2, p]
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
h : 1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1)
| HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹

Tactic:
rw [← cpow_neg_one]

Premises used: Complex.cpow_neg_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
h : ∀ (p : ℕ), 1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1)
| Tendsto (β := ℂ)
    (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

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

Premises used: Complex.cpow_neg_one, Finset.prod, mul_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
conv :
  Tendsto (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s))
    (𝓝[≠] 1) (𝓝 (HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))) 1))
⊢ Tendsto (β := ℂ)
    (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

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

Premises used: Complex.cpow_neg_one, Finset.prod, mul_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s))
    (𝓝[≠] 1) (𝓝 (HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))) 1))

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

Premises used: Filter.Tendsto.mul, riemannZeta_residue_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
refine :
  Tendsto (β := ℂ) (fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))))
⊢ Tendsto (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s))
    (𝓝[≠] 1) (𝓝 (HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))) 1))

Tactic:
refine .mul (f := fun s ↦ ∏ p ∈ N.primeFactors, _) ?_ riemannZeta_residue_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))))

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds <| Continuous.tendsto ?_ 1

Premises used: Continuous.tendsto, tendsto_nhdsWithin_of_tendsto_nhds, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
refine : Continuous (Y := ℂ) fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))))

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

Premises used: Continuous.tendsto, tendsto_nhdsWithin_of_tendsto_nhds, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
⊢ NeZero p

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦ 1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
H :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) fun (s : ℂ) ↦
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))

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

Premises used: continuous_finsetProd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Even
s : ℂ
⊢ χ.gammaFactor s = s.Gammaℝ

Tactic:
simp [gammaFactor, hχ]

Premises used: DirichletCharacter.gammaFactor
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Odd
s : ℂ
⊢ χ.gammaFactor s = (s + 1).Gammaℝ

Tactic:
simp [gammaFactor, hχ.not_even]

Premises used: DirichletCharacter.gammaFactor, DirichletCharacter.Odd.not_even
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
χ : DirichletCharacter ℂ 1
h : ∀ (x : ℂ), completedLFunction χ x = completedRiemannZeta x
⊢ completedLFunction χ = completedRiemannZeta

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

Tactic:
rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]

Premises used: DirichletCharacter.completedLFunction, map_one, ZMod.completedLFunction_modOne_eq, one_mul