awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
h : χ.Odd
neg :
  ZMod.completedLFunction (N := N) (⇑χ : (a : ZMod N) → ℂ) (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₁ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₂ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₃ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * -1 / I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₄ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    -(HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * -1 * I) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₅ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    -(-HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
⊢ completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
have neg₆ : HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
    ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
  - -HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
    ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
Tactic: rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
⊢ HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N)
        (fun (j : ZMod N) ↦
          HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
            ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
        s
have e_a : ∀ (j : ZMod N),
  (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) j =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
Tactic: congr 2 with j
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
j : ZMod N
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) j =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
have e_a : HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-j) : ℂ) (gaussSum χ stdAddChar) =
  HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
    ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
Tactic: rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
j : ZMod N
e_a :
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-j) : ℂ) (gaussSum χ stdAddChar) =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) j =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
have e_a₁ : HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1 * j) : ℂ) (gaussSum χ stdAddChar) =
  HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
    ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
Tactic: rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
j : ZMod N
e_a :
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-j) : ℂ) (gaussSum χ stdAddChar) =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
e_a₁ :
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1 * j) : ℂ) (gaussSum χ stdAddChar) =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) j =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
have e_a₂ : HMul.hMul (α := ℂ) (β := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ) *
    gaussSum χ stdAddChar =
  HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
    ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
Tactic: rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
j : ZMod N
e_a :
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-j) : ℂ) (gaussSum χ stdAddChar) =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
e_a₁ :
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1 * j) : ℂ) (gaussSum χ stdAddChar) =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
e_a₂ :
  HMul.hMul (α := ℂ) (β := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ) *
      gaussSum χ stdAddChar =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) j =
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
      ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
have e_a₃ : HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
    ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ) =
  HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
    ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ)
Tactic: rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
⊢ HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N)
        (fun (j : ZMod N) ↦
          HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
            ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
        s =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ)
have rw : HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
    (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar) *
      ZMod.completedLFunction (N := N) (⇑χ⁻¹ : (a : ZMod N) → ℂ) s) =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar *
      ZMod.completedLFunction (N := N) (⇑χ⁻¹ : (a : ZMod N) → ℂ) s *
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ)
Tactic: rw [completedLFunction, completedLFunction_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
have rw : HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
    ((χ * χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Tactic: rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
rw :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
      ((χ * χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
have rw₁ : HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
    ((1 : (a : ZMod N) → ℂ) (-1) : ℂ) =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Tactic: rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
rw :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
      ((χ * χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
rw₁ :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
      ((1 : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
have rw₂ : HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * 1 =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Tactic: rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
rw :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
      ((χ * χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
rw₁ :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s)
      ((1 : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
rw₂ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * 1 =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
have rw₃ : HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Tactic: rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
⊢ completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
      completedLFunction χ⁻¹ s
have calc : completedLFunction χ (1 - s) =
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
    ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
Tactic: calc completedLFunction χ (1 - s)
  _ = N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 χ) s := by
    simp only [ε]
    split_ifs with h
    · rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
    · replace h : χ.Odd := χ.even_or_odd.resolve_left h
      rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]
  _ = (_) * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s := by
    congr 2 with j
    rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) := by
    rw [completedLFunction, completedLFunction_const_mul]
    ring
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s := by
    rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
calc :
  completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
⊢ completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
      completedLFunction χ⁻¹ s
have calc₁ : HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
    ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
    ZMod.completedLFunction (N := N)
      (fun (j : ZMod N) ↦
        HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
          ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
      s
Tactic: calc completedLFunction χ (1 - s)
  _ = N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 χ) s := by
    simp only [ε]
    split_ifs with h
    · rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
    · replace h : χ.Odd := χ.even_or_odd.resolve_left h
      rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]
  _ = (_) * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s := by
    congr 2 with j
    rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) := by
    rw [completedLFunction, completedLFunction_const_mul]
    ring
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s := by
    rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
calc :
  completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
calc₁ :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N)
        (fun (j : ZMod N) ↦
          HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
            ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
        s
⊢ completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
      completedLFunction χ⁻¹ s
have calc₂ : HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
    ZMod.completedLFunction (N := N)
      (fun (j : ZMod N) ↦
        HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
          ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
      s =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ)
Tactic: calc completedLFunction χ (1 - s)
  _ = N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 χ) s := by
    simp only [ε]
    split_ifs with h
    · rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
    · replace h : χ.Odd := χ.even_or_odd.resolve_left h
      rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]
  _ = (_) * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s := by
    congr 2 with j
    rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) := by
    rw [completedLFunction, completedLFunction_const_mul]
    ring
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s := by
    rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]