awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
⊢ Membership.mem (γ := Filter ℂ) (𝓝 2) V

Tactic:
have hV : V ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
⊢ 2 ∈ U

Tactic:
simp [U]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
⊢ 2 ∈ U

Tactic:
have hUmem : 2 ∈ U := by simp [U]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
⊢ s ∈ U

Tactic:
have hUmem' : s ∈ U := hU.mpr hjs.symm
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s

Tactic:
hf.eqOn_of_preconnected_of_eventuallyEq hg hUc hUmem ?_ hUmem'

Premises used: AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
refine : f =ᶠ[𝓝 2] g
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s

Tactic:
refine hf.eqOn_of_preconnected_of_eventuallyEq hg hUc hUmem ?_ hUmem'

Premises used: AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
z : ℂ
⊢ z ∈ V → f z = g z

Tactic:
LFunction_stdAddChar_eq_expZeta_of_one_lt_re _

Premises used: Set.Mem, setOf, _private.0.ZMod.LFunction_stdAddChar_eq_expZeta_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ V → Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x} a
h₁ h₂ : ∀ z ∈ V, f z = g z
⊢ f =ᶠ[𝓝 2] g

Tactic:
filter_upwards [hV] with z using LFunction_stdAddChar_eq_expZeta_of_one_lt_re _

Premises used: _private.0.ZMod.LFunction_stdAddChar_eq_expZeta_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
pos :
  ∀ (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
neg :
  ∀ (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
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
by_cases h : -j ≠ 0 ∨ s ≠ 1
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : -j ≠ 0 ∨ s ≠ 1
pos pos₁ :
  Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
rw [LFunction_stdAddChar_eq_expZeta _ _ h]

Premises used: ZMod.LFunction_stdAddChar_eq_expZeta
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : ¬(-j ≠ 0 ∨ s ≠ 1)
⊢ j = 0 ∧ s = 1

Tactic:
simp only [neg_ne_zero, not_or, not_not] at h

Premises used: Classical.not_not, not_or, neg_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
inr : ∀ (hs : s ≠ 1), j = 0 → s = 1 → Φ 0 = 0
inl₁ inl₂ : ∀ (hs : Φ 0 = 0), j = 0 → s = 1 → Φ 0 = 0
⊢ Φ 0 = 0

Tactic:
tauto
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
neg₃ neg₄ : Eq (α := ℂ) 0 0
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, And.left
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
⊢ ∀ (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]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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)))
⊢ LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s =
    ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
simp only [LFunction, ← this, mul_sum]

Premises used: Finset.mul_sum, ZMod.LFunction
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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)))
⊢ 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:
rw [dft_def, sum_comm]

Premises used: Finset.sum_comm, ZMod.dft_def
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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)
⊢ 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:
simp only [sum_mul, mul_sum, smul_eq_mul, stdAddChar_apply, ← mul_assoc]

Premises used: Finset.mul_sum, mul_assoc, smul_eq_mul, Finset.sum_mul, ZMod.stdAddChar_apply
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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)
⊢ 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:
congr 1 with j
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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
⊢ 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 k
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
e_f₂ 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

Tactic:
rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]

Premises used: mul_assoc, mul_comm, neg_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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))
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))
⊢ Φ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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))
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))
⊢ Φ 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'
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
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:
simp only [hΦ, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : s ≠ 1
inl 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))
⊢ Φ 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:
rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]

Premises used: HurwitzZeta.hurwitzZeta_one_sub, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
hj : j ≠ 0
inr 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))
⊢ Φ 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:
rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]

Premises used: Iff.mpr, Iff.not, HurwitzZeta.hurwitzZeta_one_sub, Or.inl, ZMod.toAddCircle_eq_zero
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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))

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)]