awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝[>] 1) fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖

Tactic:
exact isBoundedUnder_of_eventually_ge (univ_mem' fun _ ↦ norm_nonneg _)

Premises used: Filter.isBoundedUnder_of_eventually_ge, Filter.univ_mem'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries (fun (n : ℕ) ↦ (↑(f n) : ℂ)) (↑s : ℂ)) (𝓝[>] 1) (𝓝 (↑l : ℂ))

Tactic:
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div (f := fun n ↦ f n)
    (hf.ofReal.congr fun _ ↦ ?_) fun s hs ↦ ?_

Premises used: Filter.Tendsto.ofReal, Filter.Tendsto.congr, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
refine_1 :
  ∀ (x : ℕ),
    (↑(HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 x, f k) (↑x : ℝ)) : ℂ) =
      HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 x, (fun (n : ℕ) ↦ (↑(f n) : ℂ)) k) (↑x : ℂ)
refine_2 : ∀ (s : ℝ) (hs : 1 < s), LSeriesSummable (fun (n : ℕ) ↦ (↑(f n) : ℂ)) (↑s : ℂ)
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries (fun (n : ℕ) ↦ (↑(f n) : ℂ)) (↑s : ℂ)) (𝓝[>] 1) (𝓝 (↑l : ℂ))

Tactic:
refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div (f := fun n ↦ f n)
    (hf.ofReal.congr fun _ ↦ ?_) fun s hs ↦ ?_

Premises used: Filter.Tendsto.ofReal, Filter.Tendsto.congr, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
x : ℕ
⊢ (↑(HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 x, f k) (↑x : ℝ)) : ℂ) =
    HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 x, (fun (n : ℕ) ↦ (↑(f n) : ℂ)) k) (↑x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑(f n) : ℂ)) (↑s : ℂ)

Tactic:
LSeriesSummable_of_sum_norm_bigO_and_nonneg ?_ hf' zero_le_one hs

Premises used: zero_le_one, LSeriesSummable_of_sum_norm_bigO_and_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
refine_2 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑(f n) : ℂ)) (↑s : ℂ)

Tactic:
refine LSeriesSummable_of_sum_norm_bigO_and_nonneg ?_ hf' zero_le_one hs

Premises used: zero_le_one, LSeriesSummable_of_sum_norm_bigO_and_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑(HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1) : ℝ)) atTop
    (𝓝 l)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ k ∈ Icc 1 n, f k) (↑n : ℝ)) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
exact isBigO_atTop_natCast_rpow_of_tendsto_div_rpow (by simpa)

Premises used: Asymptotics.isBigO_atTop_natCast_rpow_of_tendsto_div_rpow
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
⊢ LSeriesSummable (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s

Tactic:
LSeriesSummable_of_bounded_of_one_lt_re (fun n _ ↦ le_max' _ _ ?_) (m := c) hs

Premises used: Norm.norm, Finset.univ, Function.comp, LSeriesSummable_of_bounded_of_one_lt_re, Finset.le_max', Finset.image
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
refine : ∀ (n : ℕ), n ≠ 0 → ‖Φ (↑n : ZMod N)‖ ∈ Finset.image (norm ∘ Φ) Finset.univ
⊢ LSeriesSummable (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s

Tactic:
refine LSeriesSummable_of_bounded_of_one_lt_re (fun n _ ↦ le_max' _ _ ?_) (m := c) hs

Premises used: Norm.norm, Finset.univ, Function.comp, LSeriesSummable_of_bounded_of_one_lt_re, Finset.le_max', Finset.image
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
n : ℕ
h : n ≠ 0
⊢ ‖Φ (↑n : ZMod N)‖ ∈ Finset.image (norm ∘ Φ) Finset.univ

Tactic:
mem_image_of_mem _ (mem_univ _)

Premises used: Finset.mem_univ, Set.Mem, setOf, Finset.mem_image_of_mem
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
n : ℕ
h : n ≠ 0
⊢ ‖Φ (↑n : ZMod N)‖ ∈ Finset.image (norm ∘ Φ) Finset.univ

Tactic:
exact mem_image_of_mem _ (mem_univ _)

Premises used: Set.mem_image_of_mem, Set.mem_univ
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
Φ : ZMod 1 → ℂ
s : ℂ
⊢ LFunction Φ s = Φ 0 * riemannZeta s

Tactic:
simp only [LFunction, Nat.cast_one, one_cpow, ← singleton_eq_univ (0 : ZMod 1), sum_singleton,
    map_zero, hurwitzZeta_zero, one_mul]

Premises used: ZMod.LFunction, Finset.singleton_eq_univ, map_zero, Finset.sum_singleton, HurwitzZeta.hurwitzZeta_zero, Complex.one_cpow, OfNat.ofNat, Nat.cast_one, one_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
rw :
  Eq (α := ℂ)
    (∑ i : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ i * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
    (∑ j : ZMod N, ∑' (m : ℕ), LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m))
⊢ LFunction Φ s = LSeries (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s

Tactic:
rw [LFunction, LSeries, mul_sum, Nat.sumByResidueClasses (LSeriesSummable_of_one_lt_re Φ hs) N]

Premises used: Finset.mul_sum, Nat.sumByResidueClasses, ZMod.LFunction, LSeries, ZMod.LSeriesSummable_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
e_f :
  ∀ (j : ZMod N),
    HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) =
      ∑' (m : ℕ), LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m)
⊢ Eq (α := ℂ)
    (∑ i : ZMod N,
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ i * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
    (∑ j : ZMod N, ∑' (m : ℕ), LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m))

Tactic:
congr 1 with j
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ))

Tactic:
have : (j.val / N : ℝ) ∈ Set.Icc 0 1 := mem_Icc.mpr ⟨by positivity,
    (div_le_one (Nat.cast_pos.mpr <| NeZero.pos _)).mpr <| Nat.cast_le.mpr (val_lt j).le⟩
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℝ))
e_f :
  Eq (α := ℂ)
    (∑' (x : ℕ),
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * Φ j * (1 / ((↑x : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s))
    (∑' (m : ℕ), LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m))
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) =
    ∑' (m : ℕ), LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m)

Tactic:
rw [toAddCircle_apply, ← (hasSum_hurwitzZeta_of_one_lt_re this hs).tsum_eq, ← mul_assoc,
    ← tsum_mul_left]

Premises used: HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re, mul_assoc, tsum_mul_left, HasSum.tsum_eq, ZMod.toAddCircle_apply
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℝ))
e_f :
  ∀ (m : ℕ),
    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)
⊢ Eq (α := ℂ)
    (∑' (x : ℕ),
      HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * Φ j * (1 / ((↑x : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s))
    (∑' (m : ℕ), LSeries.term (fun (x : ℕ) ↦ Φ (↑x : ZMod N)) s (j.val + N * m))

Tactic:
congr 1 with m
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
rw :
  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)
rw₁ rw₂ :
  Φ j * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (1 / ((↑m : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s) =
    Φ j * HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (1 / ((↑m : ℂ) + (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ)) ^ s)
⊢ 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))

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

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

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

Premises used: Iff.mpr, Complex.ofReal_add, Complex.cpow_neg, mul_div_cancel_left₀, Nat.cast, add_comm, one_div, Complex.ofReal_natCast, Complex.ofReal_div, Complex.ofReal_mul, Nat.cast_ne_zero, NeZero.ne, add_div
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
ha : LE.le (α := ℝ) 0 (↑N : ℝ)
hb : 0 ≤ ((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)
⊢ Φ j *
      (1 / (↑(↑N : ℝ) : ℂ) ^ s * (1 / (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ) ^ s)) =
    Φ j / ((↑(↑N : ℝ) : ℂ) * (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ)) ^ s

Tactic:
rw [one_div_mul_one_div, mul_one_div, mul_cpow_ofReal_nonneg]

Premises used: Complex.mul_cpow_ofReal_nonneg, mul_one_div, one_div_mul_one_div
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
⊢ LE.le (α := ℝ) 0 (↑N : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
⊢ 0 ≤ ((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
⊢ Φ j / ((↑(↑N : ℝ) : ℂ) * (↑(((↑j.val : ℝ) + HMul.hMul (α := ℝ) (↑N : ℝ) (↑m : ℝ)) / (↑N : ℝ)) : ℂ)) ^ s =
    Φ j / ((↑N : ℂ) * ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) / (↑N : ℂ)) ^ s

Tactic:
simp only [ofReal_natCast, ofReal_div, ofReal_add, ofReal_mul, mul_div_assoc]

Premises used: mul_div_assoc, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_div, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
rw rw₁ :
  Φ j / ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) ^ s =
    Φ j / ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) ^ s
⊢ Φ j / ((↑N : ℂ) * ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) / (↑N : ℂ)) ^ s =
    Φ j / ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) ^ s

Tactic:
rw [mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
⊢ Φ j / ((↑j.val : ℂ) + HMul.hMul (α := ℂ) (↑N : ℂ) (↑m : ℂ)) ^ s =
    Φ (↑(j.val + N * m) : ZMod N) / HPow.hPow (α := ℂ) (↑(j.val + N * m) : ℂ) s

Tactic:
simp only [Nat.cast_add, Nat.cast_mul, natCast_zmod_val, natCast_self, zero_mul, add_zero]

Premises used: ZMod.natCast_self, MulZeroClass.zero_mul, Nat.cast_add, ZMod.natCast_zmod_val, Nat.cast_mul, add_zero
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℕ
rw rw₁ :
  Φ (↑(j.val + N * m) : ZMod N) / HPow.hPow (α := ℂ) (↑(j.val + N * m) : ℂ) s =
    Φ (↑(j.val + N * m) : ZMod N) / HPow.hPow (α := ℂ) (↑(j.val + N * m) : ℂ) s
⊢ Φ (↑(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:
rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs)]

Premises used: Complex.ne_zero_of_one_lt_re, LSeries.term_of_ne_zero'
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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)
⊢ 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)

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

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, HAdd.hAdd, LSeries.term, Neg.neg, ZMod.val
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ HPow.hPow (α := ℂ) (↑N : ℂ) (-s)) s

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
refine :
  DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s
⊢ DifferentiableAt ℂ (LFunction Φ) s

Tactic:
refine .mul (by fun_prop) ?_
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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
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
⊢ 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

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s

Tactic:
.fun_sum fun j _ ↦ (differentiableAt_hurwitzZeta _ hs').const_mul _

Premises used: DifferentiableAt.const_mul, DifferentiableAt.fun_sum, HurwitzZeta.differentiableAt_hurwitzZeta, ZMod.toAddCircle, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) s

Tactic:
exact .fun_sum fun j _ ↦ (differentiableAt_hurwitzZeta _ hs').const_mul _
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
hs : Ne (α := ℂ) 1 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
⊢ 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)
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
hs : Ne (α := ℂ) 1 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
this :
  DifferentiableAt ℂ (F := ℂ)
    (fun (y : ℂ) ↦
      ∑ i : ZMod N, Φ i * (hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) y - 1 / (y - 1) / y.Gammaℝ))
    1
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s) 1

Tactic:
simpa only [mul_sub, sum_sub_distrib, ← sum_mul, hs.neg_resolve_left rfl, zero_mul, sub_zero]

Premises used: mul_sub, sub_zero, MulZeroClass.zero_mul, Finset.sum_sub_distrib, Or.neg_resolve_left, rfl, Finset.sum_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
hΦ : Eq (α := ℂ) (∑ j : ZMod N, Φ j) 0
⊢ Differentiable ℂ (LFunction Φ)

Tactic:
fun s ↦ differentiableAt_LFunction Φ s (Or.inr hΦ)

Premises used: ZMod.differentiableAt_LFunction, Differentiable, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
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 : ℂ)))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * LFunction Φ s) (𝓝[≠] 1) (𝓝 (∑ j : ZMod N, Φ j / (↑N : ℂ)))

Tactic:
simp only [LFunction, mul_sum]

Premises used: Finset.mul_sum, ZMod.LFunction
-- Module: Mathlib.NumberTheory.LSeries.ZMod
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 : ℂ)))

Tactic:
tendsto_finsetSum _ fun j _ ↦ ?_

Premises used: tendsto_finsetSum
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
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 : ℂ)))
⊢ 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:
refine tendsto_finsetSum _ fun j _ ↦ ?_

Premises used: tendsto_finsetSum
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Φ j / (↑N : ℂ) = Φ j * (HDiv.hDiv (α := ℂ) 1 (↑N : ℂ) * 1)

Tactic:
ring