awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ))
m : ℕ
calc :
  HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * Φ j * (1 / ((↑m : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s) =
    Φ j * (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (1 / ((↑m : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s))
calc₁ :
  Φ j * (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (1 / ((↑m : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s)) =
    Φ j *
      (1 / (↑(↑N : ℝ) : ℂ) ^ s * (1 / (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ) ^ s))
calc₂ :
  Φ j *
      (1 / (↑(↑N : ℝ) : ℂ) ^ s * (1 / (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ) ^ s)) =
    Φ j / ((↑(↑N : ℝ) : ℂ) * (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ)) ^ s
calc₃ :
  Φ j / ((↑(↑N : ℝ) : ℂ) * (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ)) ^ s =
    Φ j / ((↑N : ℂ) * ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) / (↑N : ℂ)) ^ s
calc₄ :
  Φ j / ((↑N : ℂ) * ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) / (↑N : ℂ)) ^ s =
    Φ j / ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) ^ s
calc₅ :
  Φ j / ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) ^ s =
    Φ (↑(j.val + N * m) : ZMod N) / HPow.hPow (α := ℂ) (↑(j.val + N * m) : ℂ) s
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * Φ j * (1 / ((↑m : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s) =
    LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m)
have calc₆ : Φ (↑(j.val + N * m) : ZMod N) / HPow.hPow (α := ℂ) (↑(j.val + N * m) : ℂ) s =
  LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m)
Tactic: calc N ^ (-s) * Φ j * (1 / (m + (j.val / N : ℝ)) ^ s)
  _ = Φ j * (N ^ (-s) * (1 / (m + (j.val / N : ℝ)) ^ s)) := by
    rw [← mul_assoc, mul_comm _ (Φ _)]
  _ = Φ j * (1 / (N : ℝ) ^ s * (1 / ((j.val + N * m) / N : ℝ) ^ s)) := by
    simp only [cpow_neg, ← one_div, ofReal_div, ofReal_natCast, add_comm, add_div, ofReal_add,
      ofReal_mul, mul_div_cancel_left₀ (m : ℂ) (Nat.cast_ne_zero.mpr (NeZero.ne N))]
  _ = Φ j / ((N : ℝ) * ((j.val + N * m) / N : ℝ)) ^ s := by -- this is the delicate step!
    rw [one_div_mul_one_div, mul_one_div, mul_cpow_ofReal_nonneg] <;> positivity
  _ = Φ j / (N * (j.val + N * m) / N) ^ s := by
    simp only [ofReal_natCast, ofReal_div, ofReal_add, ofReal_mul, mul_div_assoc]
  _ = Φ j / (j.val + N * m) ^ s := by
    rw [mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))]
  _ = Φ ↑(j.val + N * m) / (↑(j.val + N * m)) ^ s := by
    simp only [Nat.cast_add, Nat.cast_mul, natCast_zmod_val, natCast_self, zero_mul, add_zero]
  _ = LSeries.term (Φ ·) s (j.val + N * m) := by
    rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
⊢ DifferentiableAt ℂ (LFunction Φ) s
have refine : DifferentiableAt ℂ (F := ℂ)
  (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s
Tactic: refine .mul (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s
have inl : ∀ (hs' : s ≠ 1),
  DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s
Tactic: rcases ne_or_eq s 1 with hs' | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
inl :
  ∀ (hs' : s ≠ 1),
    DifferentiableAt ℂ (F := ℂ)
      (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s
have inr : ∀ (hs : Ne (α := ℂ) 1 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0),
  DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) 1
Tactic: rcases ne_or_eq s 1 with hs' | rfl
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
hs : Ne (α := ℂ) 1 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) 1
have this : DifferentiableAt ℂ (F := ℂ)
  (fun (y : ℂ) ↦
    ∑ i : ZMod N, Φ i * (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) y - 1 / (y - 1) / y.Gammaℝ))
  1
Tactic: have := DifferentiableAt.fun_sum (u := univ) fun j _ ↦
      (differentiableAt_hurwitzZeta_sub_one_div (toAddCircle j)).const_mul (Φ j)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * LFunction Φ s) (𝓝[≠] 1) (𝓝 (∑ j : ZMod N, Φ j / (↑N : ℂ)))
have simp : Tendsto (β := ℂ)
  (fun (s : ℂ) ↦
    ∑ i : ZMod N,
      (s - 1) *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ i * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s)))
  (𝓝[≠] 1) (𝓝 (∑ j : ZMod N, Φ j / (↑N : ℂ)))
Tactic: simp only [LFunction, mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (β := ℂ)
    (fun (s : ℂ) ↦
      ∑ i : ZMod N,
        (s - 1) *
          (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ i * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s)))
    (𝓝[≠] 1) (𝓝 (∑ j : ZMod N, Φ j / (↑N : ℂ)))
have refine : ∀ (j : ZMod N),
  Membership.mem (γ := Finset (ZMod N)) Finset.univ j →
    Tendsto
      (fun (s : ℂ) ↦
        (s - 1) *
          (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
      (𝓝[≠] 1) (𝓝 (Φ j / (↑N : ℂ)))
Tactic: refine tendsto_finsetSum _ fun j _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - 1) *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j / (↑N : ℂ)))
have rw : Tendsto
  (fun (s : ℂ) ↦
    (s - 1) *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
  (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))
Tactic: rw [(by ring : Φ j / N = Φ j * (1 / N * 1)), one_div, ← cpow_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - 1) *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))
have simp : Tendsto
  (fun (s : ℂ) ↦
    Φ j *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * ((s - 1) * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
  (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))
Tactic: simp only [show ∀ a b c d : ℂ, a * (b * (c * d)) = c * (b * (a * d)) by intros; ring]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Tendsto
    (fun (s : ℂ) ↦
      Φ j *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * ((s - 1) * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))
have refine : Tendsto (fun (s : ℂ) ↦ HPow.hPow (α := ℂ) (↑N : ℂ) (-s)) (𝓝[≠] 1) (𝓝 (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1)))
Tactic: refine tendsto_const_nhds.mul (.mul ?_ <| hurwitzZeta_residue_one _)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have rw : Eq (α := ℂ) (∑' (n : ℕ), LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n)
  (∑' (b : ℕ),
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑b : ℂ)) /
      HPow.hPow (α := ℂ) (↑b : ℂ) s)
Tactic: rw [toAddCircle_apply, ← (hasSum_expZeta_of_one_lt_re (j.val / N) hs).tsum_eq,
    LFunction_eq_LSeries _ hs, LSeries]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ Eq (α := ℂ) (∑' (n : ℕ), LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n)
    (∑' (b : ℕ),
      cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑b : ℂ)) /
        HPow.hPow (α := ℂ) (↑b : ℂ) s)
have e_f : ∀ (n : ℕ),
  LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n =
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑n : ℂ)) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: congr 1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n =
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑n : ℂ)) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_f : (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), ofReal_div, ofReal_natCast,
    ofReal_natCast, mul_assoc, div_mul_eq_mul_div, stdAddChar_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have this : (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
  cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))
Tactic: have := ZMod.toCircle_intCast (N := N) (j.val * n)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))
| cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))
have rw : cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
Tactic: rw [Int.cast_mul, Int.cast_natCast, Int.cast_natCast, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have this₁ : (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
  cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
Tactic: conv_rhs at this => rw [Int.cast_mul, Int.cast_natCast, Int.cast_natCast, mul_div_assoc]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_f : (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) /
    HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
e_f :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_f₁ : (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑(↑j.val : ℤ) : ZMod N) (↑(↑n : ℤ) : ZMod N))) : ℂ) /
    HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
e_f :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₁ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑(↑j.val : ℤ) : ZMod N) (↑(↑n : ℤ) : ZMod N))) :
        ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_f₂ : (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑(↑n : ℤ) : ZMod N))) : ℂ) /
    HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
e_f :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₁ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑(↑j.val : ℤ) : ZMod N) (↑(↑n : ℤ) : ZMod N))) :
        ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₂ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑(↑n : ℤ) : ZMod N))) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_f₃ : (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑n : ZMod N))) : ℂ) /
    HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
e_f :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₁ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑(↑j.val : ℤ) : ZMod N) (↑(↑n : ℤ) : ZMod N))) :
        ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₂ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑(↑n : ℤ) : ZMod N))) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₃ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑n : ZMod N))) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_f₄ : (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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}
⊢ IsOpen U
have pos : ∀ (h : j = 0), IsOpen U
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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}
pos : ∀ (h : j = 0), IsOpen U
⊢ IsOpen U
have neg : ∀ (h : ¬j = 0), IsOpen U
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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}
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hUo : IsOpen U
Tactic: have hUo : IsOpen U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using isOpen_compl_singleton
    · simp only [h, ↓reduceIte, isOpen_univ, U]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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)
u : ℂ
⊢ u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
have simp : j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
Tactic: simp only [mem_ite_univ_right, U]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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)
u : ℂ
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inl : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
Tactic: tauto
Cleared hypotheses: hjs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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)
u : ℂ
inl : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inr : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
Tactic: tauto
Cleared hypotheses: hjs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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)
u : ℂ
inl : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₁ : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr₁ : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inl₂ : ∀ (hjs : j ≠ 0), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
Tactic: tauto
Cleared hypotheses: hjs