awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)

Tactic:
have := χ.map_zero'
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0

Tactic:
have := χ.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
⊢ Differentiable ℂ (completedLFunction χ)

Tactic:
fun s ↦ differentiableAt_completedLFunction _ _ (Or.inr ?_) (Or.inr hχ)

Premises used: Differentiable, DirichletCharacter.differentiableAt_completedLFunction, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
refine : ∀ (s : ℂ), N ≠ 1
⊢ Differentiable ℂ (completedLFunction χ)

Tactic:
refine fun s ↦ differentiableAt_completedLFunction _ _ (Or.inr ?_) (Or.inr hχ)

Premises used: DirichletCharacter.differentiableAt_completedLFunction, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
s : ℂ
⊢ N ≠ 1

Tactic:
hχ ∘ level_one' _

Premises used: DirichletCharacter.level_one', Function.comp, Not
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
s : ℂ
⊢ N ≠ 1

Tactic:
exact hχ ∘ level_one' _

Premises used: DirichletCharacter.level_one'
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
inl : ∀ (hχ : χ.Even), LFunction χ s = completedLFunction χ s / χ.gammaFactor s
inr : ∀ (hχ : χ.Odd), LFunction χ s = completedLFunction χ s / χ.gammaFactor s
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
rcases χ.even_or_odd with hχ | hχ

Premises used: DirichletCharacter.even_or_odd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
inl : LFunction χ s = completedLFunction χ s / s.Gammaℝ
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
rw [hχ.gammaFactor_def]

Premises used: DirichletCharacter.Even.gammaFactor_def
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
inr : LFunction χ s = completedLFunction χ s / (s + 1).Gammaℝ
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
rw [hχ.gammaFactor_def]

Premises used: DirichletCharacter.Odd.gammaFactor_def
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / s.Gammaℝ

Tactic:
LFunction_eq_completed_div_gammaFactor_even hχ.to_fun _ (h.imp_right χ.map_zero')

Premises used: DirichletCharacter.completedLFunction, ZMod.LFunction_eq_completed_div_gammaFactor_even, DirichletCharacter.LFunction, DirichletCharacter.Even.to_fun, DirichletCharacter.map_zero', Or.imp_right
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / s.Gammaℝ

Tactic:
exact LFunction_eq_completed_div_gammaFactor_even hχ.to_fun _ (h.imp_right χ.map_zero')

Premises used: ZMod.LFunction_eq_completed_div_gammaFactor_even, DirichletCharacter.Even.to_fun, DirichletCharacter.map_zero', Or.imp_right
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / (s + 1).Gammaℝ

Tactic:
apply LFunction_eq_completed_div_gammaFactor_odd hχ.to_fun

Premises used: DirichletCharacter.Odd.to_fun, ZMod.LFunction_eq_completed_div_gammaFactor_odd
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
χ : DirichletCharacter ℂ 1
⊢ χ.rootNumber = 1

Tactic:
simp [rootNumber, gaussSum, -univ_unique, ← singleton_eq_univ (1 : ZMod 1),
    (show stdAddChar (1 : ZMod 1) = 1 from AddChar.map_zero_eq_one _),
    (show χ.Even from map_one _)]

Premises used: ZMod.stdAddChar, Finset.singleton_eq_univ, Finset.univ_unique, AddChar.map_zero_eq_one, map_one, DirichletCharacter.rootNumber, gaussSum, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
inl :
  ∀ [inst : NeZero (R := ℕ) 1] {χ : DirichletCharacter ℂ 1} (hχ : χ.IsPrimitive),
    completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑1 : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
inr :
  ∀ (hN : N ≠ 1),
    completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
rcases eq_or_ne N 1 with rfl | hN

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
s : ℂ
inst : NeZero (R := ℕ) 1
χ : DirichletCharacter ℂ 1
hχ : χ.IsPrimitive
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑1 : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
simp [completedLFunction_modOne_eq, completedRiemannZeta_one_sub, rootNumber_modOne]

Premises used: DirichletCharacter.rootNumber_modOne, DirichletCharacter.completedLFunction_modOne_eq, completedRiemannZeta_one_sub
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0

Tactic:
χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)

Premises used: Ne.symm, MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
refine : ∀ (h : χ = 1), 1 = N
⊢ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0

Tactic:
refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)

Premises used: Ne.symm, MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h : χ = 1
rwa : ∀ (hχ : χ.conductor = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
rwa₁ : ∀ (hχ : conductor (R := ℂ) (n := N) 1 = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hχ : 1 = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
⊢ 1 = N

Tactic:
rwa [IsPrimitive, h, conductor_one] at hχ

Premises used: DirichletCharacter.conductor_one, DirichletCharacter.IsPrimitive
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0

Tactic:
have h_sum : ∑ j, χ j = 0 := by
    refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
    rwa [IsPrimitive, h, conductor_one] at hχ
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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)
inr :
  completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
      completedLFunction χ⁻¹ s
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
rw [rootNumber, ← mul_comm_div, ← mul_comm_div, ← cpow_sub _ _ (NeZero.ne _), sub_sub, add_halves]

Premises used: add_halves, Complex.cpow_sub, sub_sub, mul_comm_div, DirichletCharacter.rootNumber, NeZero.ne
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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)
simp :
  completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) *
      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) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s

Tactic:
simp only [ε]
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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)
pos :
  ∀ (h : χ.Even),
    completedLFunction χ (1 - s) =
      HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
          HPow.hPow (β := ℕ) I 0 *
        ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg :
  ∀ (h : ¬χ.Even),
    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
⊢ completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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 : χ.Even
pos :
  completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
pos₁ :
  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
pos₂ :
  completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
pos₃ :
  completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
pos₄ :
  ZMod.completedLFunction (N := N) (⇑χ : (a : ZMod N) → ℂ) (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
pos₅ pos₆ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
      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 0 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s

Tactic:
rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]

Premises used: DirichletCharacter.completedLFunction, pow_zero, mul_one, ZMod.completedLFunction_one_sub_even, DirichletCharacter.Even.to_fun, DirichletCharacter.map_zero', div_one, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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 : ¬χ.Even
⊢ χ.Odd

Tactic:
replace h : χ.Odd := χ.even_or_odd.resolve_left h
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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)
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 : ℂ)
⊢ 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:
congr 2 with j
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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 : ℂ)
e_a₃ 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 : ℂ)
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (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]

Premises used: neg_one_mul, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, map_mul, mul_right_comm
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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)) ((χ : (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) : ℂ)
⊢ 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:
rw [completedLFunction, completedLFunction_const_mul]

Premises used: DirichletCharacter.completedLFunction, ZMod.completedLFunction_const_mul
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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) : ℂ) / ε *
      (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:
ring
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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
rw₃ rw₄ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s =
    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

Tactic:
rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]

Premises used: MulChar.mul_apply, MulChar.one_apply, isUnit_one, mul_inv_cancel, IsUnit.neg, mul_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
inl :
  ∀ [inst : NeZero (R := ℕ) 1] {χ : DirichletCharacter ℂ 1} (hχ : χ.IsPrimitive),
    completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑1 : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
inr inr₁ :
  ∀ (hN : N ≠ 1),
    completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
inr₂ inr₃ :
  ∀ (hN : N ≠ 1) (h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0),
    completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
inr₄ :
  ∀ (hN : N ≠ 1) (h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0),
    completedLFunction χ (1 - s) =
      HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
        completedLFunction χ⁻¹ s
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
classical
  -- First handle special case of Riemann zeta
  rcases eq_or_ne N 1 with rfl | hN
  · simp [completedLFunction_modOne_eq, completedRiemannZeta_one_sub, rootNumber_modOne]
  -- facts about `χ` as function
  have h_sum : ∑ j, χ j = 0 := by
    refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
    rwa [IsPrimitive, h, conductor_one] at hχ
  let ε := I ^ (if χ.Even then 0 else 1)
  -- gather up powers of N
  rw [rootNumber, ← mul_comm_div, ← mul_comm_div, ← cpow_sub _ _ (NeZero.ne _), sub_sub, add_halves]
  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]

Premises used: ZMod.completedLFunction, DirichletCharacter.completedLFunction, HMul.hMul, add_halves, ZMod.stdAddChar, ZMod.dft, HSub.hSub, Complex.cpow_sub, sub_sub, Inv.inv, mul_comm_div, DirichletCharacter.rootNumber, gaussSum, eq_or_ne, DirichletCharacter.rootNumber_modOne, DirichletCharacter.completedLFunction_modOne_eq, OfNat.ofNat, DFunLike.coe, Neg.neg, rfl, completedRiemannZeta_one_sub, NeZero.ne
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
simp : Ne (α := ℂ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 0
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
simp only [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
⊢ Ne (α := ℂ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 0

Tactic:
Finset.prod_ne_zero_iff.mpr fun p hp ↦ ?_

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
refine : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹ ≠ 0
⊢ Ne (α := ℂ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹) 0

Tactic:
refine Finset.prod_ne_zero_iff.mpr fun p hp ↦ ?_

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
p : ℕ
hp : p ∈ n.primeFactors
⊢ HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹ ≠ 0

Tactic:
simpa [sub_ne_zero] using (Nat.prime_of_mem_primeFactors hp).ne_one

Premises used: sub_ne_zero, Nat.prime_of_mem_primeFactors, Nat.Prime.ne_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
rw : DifferentiableOn ℂ (LFunctionTrivChar₁ n) (Set.univ \ {1}) ∧ ContinuousAt (LFunctionTrivChar₁ n) 1
⊢ Differentiable ℂ (LFunctionTrivChar₁ n)

Tactic:
rw [← differentiableOn_univ,
    ← differentiableOn_compl_singleton_and_continuousAt_iff (c := 1) Filter.univ_mem]

Premises used: differentiableOn_univ, Complex.differentiableOn_compl_singleton_and_continuousAt_iff, Filter.univ_mem