awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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
have refine_2 : DifferentiableAt ℂ (F := ℂ)
  (fun (s : ℂ) ↦
    ∏ p ∈ N.primeFactors,
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
  s
Tactic: refine ((differentiableAt_LFunction _ _ (.inl hs)).mul ?_).differentiableWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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
have 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
Tactic: refine .fun_finsetProd fun i h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
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
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑i : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑i : ℂ) (-s)))
    s
have this : NeZero i
Tactic: have : NeZero i := ⟨(Nat.pos_of_mem_primeFactors h).ne'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)))
have refine_3 : Membership.mem (γ := Filter ℂ) (𝓝 2) fun (t : ℂ) ↦ Real.lt✝ 1 t.re
Tactic: refine eventually_of_mem ?_ (fun t (ht : 1 < t.re) ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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
⊢ 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)))
have 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
Tactic: refine eventually_of_mem ?_ (fun t (ht : 1 < t.re) ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1 ∨ 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)))
have 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)))
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
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)))
have hχ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
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
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦
    1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
have this : NeZero p
Tactic: have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
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)
⊢ 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)))
have h' : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * riemannZeta s
have rw : LFunction (N := N) ((changeLevel sorry : (a : DirichletCharacter ℂ 1) → DirichletCharacter ℂ N) 1) s =
  LFunction (N := 1) 1 s * ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
Tactic: rw [← LFunction_modOne_eq (χ := 1), LFunctionTrivChar, ← changeLevel_one N.one_dvd, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
have h : ∀ p ∈ N.primeFactors,
  HPow.hPow (α := ℂ) (↑p : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑p : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
Tactic: convert! LFunction_changeLevel N.one_dvd 1 (.inr hs) using 4 with p
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
h : p ∈ N.primeFactors
⊢ HPow.hPow (α := ℂ) (↑p : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑p : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
have h : HPow.hPow (α := ℂ) (↑p : ℂ) (-s) = 1 * HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
Tactic: rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
⊢ HPow.hPow (α := ℂ) (↑p : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑p : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
have h₁ : HPow.hPow (α := ℂ) (↑p : ℂ) (-s) = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
Tactic: rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
have 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)
Tactic: refine Set.EqOn.eventuallyEq_nhdsWithin fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
s : ℂ
hs : Membership.mem (γ := Set ℂ) {1}ᶜ s
⊢ (s - 1) * LFunctionTrivChar N s =
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
have rw : (s - 1) * LFunctionTrivChar N s =
  (s - 1) * ((∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * riemannZeta s)
Tactic: rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
⊢ (s - 1) * LFunctionTrivChar N s =
    (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)
have 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)
Tactic: rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
N : ℕ
inst : NeZero N
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have H : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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 : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have rw : Tendsto (β := ℂ)
  (fun (s : ℂ) ↦ (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
  (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
Tactic: rw [tendsto_congr' H]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have enter : ∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹
Tactic: enter [3, 1]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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 ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹
have rw : HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 1
Tactic: rw [← mul_one <| Finset.prod ..]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
| HMul.hMul (α := ℂ) (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 1
have h : ∀ (p : ℕ), HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹
Tactic: enter [1, 2, p]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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 : ℕ
| HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹
have h : 1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1)
Tactic: rw [← cpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have h : ∀ (p : ℕ), 1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1)
Tactic: enter [3, 1]; rw [← mul_one <| Finset.prod ..]; enter [1, 2, p]; rw [← cpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have 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))
Tactic: conv => enter [3, 1]; rw [← mul_one <| Finset.prod ..]; enter [1, 2, p]; rw [← cpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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))
have refine : Tendsto (β := ℂ) (fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))) (𝓝[≠] 1)
  (𝓝 (∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (β := ℂ) (↑p : ℂ) (-1))))
Tactic: refine .mul (f := fun s ↦ ∏ p ∈ N.primeFactors, _) ?_ riemannZeta_residue_one
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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))))
have refine : Continuous (Y := ℂ) fun (s : ℂ) ↦ ∏ p ∈ N.primeFactors, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))
Tactic: refine tendsto_nhdsWithin_of_tendsto_nhds <| Continuous.tendsto ?_ 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
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
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦ 1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
have this : NeZero p
Tactic: have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
⊢ completedLFunction χ = completedRiemannZeta
have h : ∀ (x : ℂ), completedLFunction χ x = completedRiemannZeta x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
⊢ completedLFunction χ x = completedRiemannZeta x
have h : ZMod.completedLFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = completedRiemannZeta x
Tactic: rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
h : ZMod.completedLFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = completedRiemannZeta x
⊢ completedLFunction χ x = completedRiemannZeta x
have h₁ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 1 : ℂ) (completedRiemannZeta x) = completedRiemannZeta x
Tactic: rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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
⊢ completedLFunction χ x = completedRiemannZeta x
have h₂ : 1 * completedRiemannZeta x = completedRiemannZeta x
Tactic: rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
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
⊢ completedLFunction χ x = completedRiemannZeta x
have h₃ : completedRiemannZeta x = completedRiemannZeta x
Tactic: rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have this : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: have := χ.map_zero'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₁ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₃ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this