awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * (2 * (↑π : ℂ)) ^ (-s) * Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
have simp : HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
    ∑ x : ZMod N,
      Φ x *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * ((2 * (↑π : ℂ)) ^ (-s) * Gamma s) *
    (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
      cexp (-(↑π : ℂ) * I * s / 2) *
        LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
Tactic: simp only [this, mul_assoc _ _ (Gamma s)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
            (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * ((2 * (↑π : ℂ)) ^ (-s) * Gamma s) *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
have generalize : ∀ (C : ℂ),
  HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          (C *
            (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * C *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
Tactic: generalize (2 * π) ^ (-s) * Gamma s = C
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          (C *
            (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * C *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
have simp_rw : C *
    (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
      ∑ x : ZMod N,
        Φ x *
          (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
            cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
  C *
    (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
      (cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * (I * s) / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s))
Tactic: simp_rw [← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc,
    neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ C *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
        ∑ x : ZMod N,
          Φ x *
            (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    C *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
        (cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
          cexp (-(↑π : ℂ) * (I * s) / 2) *
            LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s))
have e_a : ∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
  cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s
have e_a : ∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
  cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
Tactic: rw [LFunction_dft _ hs', LFunction_dft _ (hs'.imp_left <| by simp only [neg_zero, imp_self])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
| cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have enter : ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
Tactic: enter [2, 2]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
| ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have rw : ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
Tactic: rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
| cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have enter : ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
Tactic: enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have e_a : ∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
  cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
Tactic: conv_rhs => enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
have e_a : ∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
  cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) * ∑ x : ZMod N, Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s
Tactic: simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
    ← mul_add, map_neg, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) * ∑ x : ZMod N, Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
have e_a₁ : ∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
  HAdd.hAdd (α := ℂ)
    (∑ i : ZMod N,
      cexp ((↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-i)) s))
    (∑ i : ZMod N, cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
Tactic: simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
    ← mul_add, map_neg, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) * ∑ x : ZMod N, Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s
e_a₁ :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    HAdd.hAdd (α := ℂ)
      (∑ i : ZMod N,
        cexp ((↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-i)) s))
      (∑ i : ZMod N,
        cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
have e_a₂ : Eq (α := ℂ)
  (∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
  (∑ x : ZMod N,
    (cexp ((↑π : ℂ) * (I * s) / 2) * (Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-x)) s) +
      cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)))
Tactic: simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
    ← mul_add, map_neg, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) * ∑ x : ZMod N, Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s
e_a₁ :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    HAdd.hAdd (α := ℂ)
      (∑ i : ZMod N,
        cexp ((↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-i)) s))
      (∑ i : ZMod N,
        cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
e_a₂ :
  Eq (α := ℂ)
    (∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
    (∑ x : ZMod N,
      (cexp ((↑π : ℂ) * (I * s) / 2) * (Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-x)) s) +
        cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)))
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
have e_a₃ : Eq (α := ℂ)
  (∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
  (∑ x : ZMod N,
    (cexp ((↑π : ℂ) * I * s / 2) * Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-x)) s +
      cexp (-(↑π : ℂ) * I * s / 2) * Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
Tactic: simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
    ← mul_add, map_neg, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (goal)
Goal:
⊢ Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ
have refine_1 : riemannZeta 2 ≠ 0
Tactic: refine analyticOn_riemannZeta.preimage_zero_mem_codiscreteWithin (x := 2) ?_ (by simp) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (goal)
Goal:
refine_1 : riemannZeta 2 ≠ 0
⊢ Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ
have refine_2 : IsConnected (α := ℂ) {1}ᶜ
Tactic: refine analyticOn_riemannZeta.preimage_zero_mem_codiscreteWithin (x := 2) ?_ (by simp) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (hypothesis)
Goal:
⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ
have this : Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ
Tactic: have := riemannZetaZeros_codiscreteWithin_compl_one
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (goal)
Goal:
this : Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ
⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ
have simp : ∀ (this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ) (x : ℂ),
  riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
Tactic: simp only [mem_codiscreteWithin, Set.mem_compl_iff, Set.mem_singleton_iff, sdiff_compl,
    Set.inf_eq_inter, Filter.disjoint_principal_right, mem_codiscrete, compl_compl] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (goal)
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
have inl : Membership.mem (γ := Filter ℂ) (nhdsWithin 1 {1}ᶜ) riemannZetaZerosᶜ
Tactic: rcases eq_or_ne x 1 with rfl | hx
Cleared hypotheses: x