awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : ¬(-j ≠ 0 ∨ s ≠ 1)
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have h₁ : j = 0 ∧ s = 1
Tactic: simp only [neg_ne_zero, not_or, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ Φ 0 = 0
have inl : ∀ (hs : Φ 0 = 0), j = 0 → s = 1 → Φ 0 = 0
Tactic: tauto
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
inl : ∀ (hs : Φ 0 = 0), j = 0 → s = 1 → Φ 0 = 0
⊢ Φ 0 = 0
have inr : ∀ (hs : s ≠ 1), j = 0 → s = 1 → Φ 0 = 0
Tactic: tauto
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have neg : Φ 0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
  Φ 0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
Tactic: rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
neg :
  Φ 0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
    Φ 0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have neg₁ : 0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
  0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
Tactic: rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
neg :
  Φ 0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
    Φ 0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
neg₁ :
  0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
    0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have neg₂ : 0 = 0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
Tactic: rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
neg :
  Φ 0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
    Φ 0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
neg₁ :
  0 * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-0 * k)) s =
    0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
neg₂ : 0 = 0 * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-0)) s
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have neg₃ : Eq (α := ℂ) 0 0
Tactic: rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
⊢ LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s =
    ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have this : ∀ (j : ZMod N),
  Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
Tactic: have (j : ZMod N) : Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s =
      Φ j * expZeta (toAddCircle (-j)) s := by
    by_cases h : -j ≠ 0 ∨ s ≠ 1
    · rw [LFunction_stdAddChar_eq_expZeta _ _ h]
    · simp only [neg_ne_zero, not_or, not_not] at h
      rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s =
    ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have simp : Eq (α := ℂ)
  (∑ i : ZMod N,
    HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
      HMul.hMul (α := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ i : ℂ)
        (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
  (∑ x : ZMod N,
    ∑ i : ZMod N,
      Φ x *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
          HMul.hMul (α := ℂ) ((𝕖 : (a : ZMod N) → ℂ) (-x * i) : ℂ)
            (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s)))
Tactic: simp only [LFunction, ← this, mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ Eq (α := ℂ)
    (∑ i : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
        HMul.hMul (α := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ i : ℂ)
          (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
    (∑ x : ZMod N,
      ∑ i : ZMod N,
        Φ x *
          (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
            HMul.hMul (α := ℂ) ((𝕖 : (a : ZMod N) → ℂ) (-x * i) : ℂ)
              (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s)))
have rw : Eq (α := ℂ)
  (∑ i : ZMod N,
    HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
      ((fun (k : ZMod N) ↦ (∑ j : ZMod N, HSMul.hSMul (α := ℂ) ((𝕖 : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ j) : ℂ)) i *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
  (∑ y : ZMod N,
    ∑ x : ZMod N,
      Φ x *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
          HMul.hMul (α := ℂ) ((𝕖 : (a : ZMod N) → ℂ) (-x * y) : ℂ)
            (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) y) s)))
Tactic: rw [dft_def, sum_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ Eq (α := ℂ)
    (∑ i : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
        ((fun (k : ZMod N) ↦ (∑ j : ZMod N, HSMul.hSMul (α := ℂ) ((𝕖 : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ j) : ℂ)) i *
          hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
    (∑ y : ZMod N,
      ∑ x : ZMod N,
        Φ x *
          (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) *
            HMul.hMul (α := ℂ) ((𝕖 : (a : ZMod N) → ℂ) (-x * y) : ℂ)
              (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) y) s)))
have simp : Eq (α := ℂ)
  (∑ x : ZMod N,
    ∑ x_1 : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(x_1 * x))) : ℂ) * Φ x_1 *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)
  (∑ x : ZMod N,
    ∑ x_1 : ZMod N,
      Φ x_1 * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-x_1 * x)) : ℂ) *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)
Tactic: simp only [sum_mul, mul_sum, smul_eq_mul, stdAddChar_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ Eq (α := ℂ)
    (∑ x : ZMod N,
      ∑ x_1 : ZMod N,
        HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(x_1 * x))) : ℂ) * Φ x_1 *
          hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)
    (∑ x : ZMod N,
      ∑ x_1 : ZMod N,
        Φ x_1 * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-x_1 * x)) : ℂ) *
          hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)
have e_f : ∀ (j : ZMod N),
  Eq (α := ℂ)
    (∑ x : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(x * j))) : ℂ) * Φ x *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)
    (∑ x : ZMod N,
      Φ x * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-x * j)) : ℂ) *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)
Tactic: congr 1 with j
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
j : ZMod N
⊢ Eq (α := ℂ)
    (∑ x : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(x * j))) : ℂ) * Φ x *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)
    (∑ x : ZMod N,
      Φ x * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-x * j)) : ℂ) *
        hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)
have e_f : ∀ (k : ZMod N),
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    Φ k * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ) *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
Tactic: congr 1 with k
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
j k : ZMod N
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    Φ k * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ) *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have e_f : HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
    hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
  Φ k * (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ)) *
    hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
Tactic: rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
j k : ZMod N
e_f :
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    Φ k * (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ)) *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    Φ k * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ) *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have e_f₁ : HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
    hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ) * Φ k *
    hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
Tactic: rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
j k : ZMod N
e_f :
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    Φ k * (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ)) *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
e_f₁ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
    Φ k * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-k * j)) : ℂ) *
      hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have e_f₂ : HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
    hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s =
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) * Φ k *
    hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
Tactic: rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]
-- 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
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))
have inl : Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
  Φ 0 *
    ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
      (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
        cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
Tactic: rcases eq_or_ne j 0 with rfl | hj
Cleared hypotheses: j
-- 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
j : ZMod N
inl :
  Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
    Φ 0 *
      ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
⊢ Φ 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))
have inr : ∀ (hj : j ≠ 0),
  Φ 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))
Tactic: rcases eq_or_ne j 0 with rfl | hj
-- 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
⊢ Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
    Φ 0 *
      ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
have inl : ∀ (hΦ : Φ 0 = 0),
  Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
    Φ 0 *
      ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
Tactic: rcases hs' with hΦ | hs'
Cleared hypotheses: hs'
-- 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
inl :
  ∀ (hΦ : Φ 0 = 0),
    Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
      Φ 0 *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
⊢ Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
    Φ 0 *
      ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
have inl₁ : ∀ (hs' : s ≠ 1),
  Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
    Φ 0 *
      ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
Tactic: rcases hs' with hΦ | hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : s ≠ 1
⊢ Φ 0 * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) (1 - s) =
    Φ 0 *
      ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
have inl : Φ 0 *
    ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
      (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
        cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s)) =
  Φ 0 *
    ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
      (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s +
        cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) 0) s))
Tactic: rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]
-- 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
j : ZMod N
hj : j ≠ 0
⊢ Φ 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))
have inr : Φ 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)) =
  Φ 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))
Tactic: rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ 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 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))
Tactic: have (j : ZMod N) : Φ j * hurwitzZeta (toAddCircle j) (1 - s) = Φ j *
      ((2 * π) ^ (-s) * Gamma s * (cexp (-π * I * s / 2) *
      expZeta (toAddCircle j) s + cexp (π * I * s / 2) * expZeta (-toAddCircle j) s)) := by
    rcases eq_or_ne j 0 with rfl | hj
    · rcases hs' with hΦ | hs'
      · simp only [hΦ, zero_mul]
      · rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]
    · rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]