awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ EventuallyEq (β := ℂ) atTop
    (fun (x : ℝ) ↦
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) x *
        (↑((↑⌊x⌋₊ : ℝ) / x) : ℂ))
    fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)
have h : ∀ (t : ℝ) (ht : 1 ≤ t),
  ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) t * (↑((↑⌊t⌋₊ : ℝ) / t) : ℂ) =
    (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)
Tactic: filter_upwards [eventually_ge_atTop 1] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (t : ℝ) in atTop, ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
Tactic: have h_lim' : Tendsto (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k : ℂ) / t) atTop (𝓝 l) := by
    refine (mul_one l ▸ ofReal_one ▸ ((hlim.comp tendsto_nat_floor_atTop).mul <|
      tendsto_ofReal_iff.mpr <| tendsto_nat_floor_div_atTop)).congr' ?_
    filter_upwards [eventually_ge_atTop 1] with t ht
    simp [div_mul_div_cancel₀ (show (⌊t⌋₊ : ℂ) ≠ 0 by simpa)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
⊢ ∀ᶠ (t : ℝ) in atTop, ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h : ∀ (t : ℝ) (ht₁ : 0 < t) (ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε),
  ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: filter_upwards [eventually_gt_atTop 0, Metric.tendsto_nhds.mp h_lim' ε hε] with t ht₁ ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h₂ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖(↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₂ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖(↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h₃ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖t‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₂ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖(↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₃ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖t‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h₄ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₂ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖(↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₃ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖t‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₄ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h₅ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₂ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖(↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₃ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖t‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₄ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₅ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
have h₆ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
Tactic: rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε
have hT₀ : 0 < T
Tactic: have hT₀ : 0 < T := zero_lt_one.trans_le hT₁
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
t : ℝ
ht : 0 < t
⊢ t ^ (-s) = t * t ^ (-s - 1)
have rw : t ^ (-s) = t * (t ^ (-s) / HPow.hPow (β := ℝ) t 1)
Tactic: rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
t : ℝ
ht : 0 < t
rw : t ^ (-s) = t * (t ^ (-s) / HPow.hPow (β := ℝ) t 1)
⊢ t ^ (-s) = t * t ^ (-s - 1)
have rw₁ : t ^ (-s) = t * (t ^ (-s) / t)
Tactic: rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
t : ℝ
ht : 0 < t
rw : t ^ (-s) = t * (t ^ (-s) / HPow.hPow (β := ℝ) t 1)
rw₁ : t ^ (-s) = t * (t ^ (-s) / t)
⊢ t ^ (-s) = t * t ^ (-s - 1)
have rw₂ : t ^ (-s) = t ^ (-s)
Tactic: rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε
have h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
Tactic: have h {t : ℝ} (ht : 0 < t) : t ^ (-s) = t * t ^ (-s - 1) := by
    rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)
have refine_1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
  (Set.Ioi T) volume
Tactic: refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioi T) volume
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)
have refine_2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ε * t ^ (-s)) (Set.Ioi T) volume
Tactic: refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioi T) volume
refine_2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ε * t ^ (-s)) (Set.Ioi T) volume
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)
have refine_3 : ∀ (t : ℝ) (ht : t ∈ Set.Ioi T), ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
Tactic: refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
have ht' : 0 < t
Tactic: have ht' : 0 < t := hT₀.trans ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
⊢ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
have refine_3 : ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t * t ^ (-s - 1)
Tactic: rw [h ht', ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ε * t ^ (-s)) ≤
    ε *
      ((s - 1) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s))
have rw : ((s - 1) * ε *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (a : ℝ) ↦ a ^ (-s)) ≤
  (s - 1) * ε *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)
Tactic: rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ ((s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (a : ℝ) ↦ a ^ (-s)) ≤
    (s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)
have refine_1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ (-s)) (Set.Ioi 1) volume
Tactic: refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
refine_1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ (-s)) (Set.Ioi 1) volume
⊢ ((s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (a : ℝ) ↦ a ^ (-s)) ≤
    (s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)
have refine_2 : (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioi 1))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ a ^ (-s)
Tactic: refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ ε *
      ((s - 1) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)) =
    ε
have rw : ε * ((s - 1) * (-1 / (-s + 1))) = ε
Tactic: rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ -s + 1 ≠ 0
have linarith : -s + 1 = 0 → 1 - s + -(-s + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε
have _ : ((s - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
      ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
  (s - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)
Tactic: calc
    _ ≤ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ε * t ^ (-s) := by
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
      · exact (lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁
      · exact (integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) hT₀).const_mul _
      · have ht' : 0 < t := hT₀.trans ht
        rw [h ht', ← mul_assoc]
        exact mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)
    _ ≤ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) := by
      rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
      · exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one
      · exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _
    _ = ε := by
      rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
      field [show -s + 1 ≠ 0 by linarith]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
_ :
  ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε
have _₁ : ((s - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)) ≤
  ε *
    ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s))
Tactic: calc
    _ ≤ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ε * t ^ (-s) := by
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
      · exact (lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁
      · exact (integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) hT₀).const_mul _
      · have ht' : 0 < t := hT₀.trans ht
        rw [h ht', ← mul_assoc]
        exact mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)
    _ ≤ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) := by
      rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
      · exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one
      · exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _
    _ = ε := by
      rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
      field [show -s + 1 ≠ 0 by linarith]