awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₅ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * x ^ (-(s + 1))
rw₆ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
rw₇ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
rw₈ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
rw₉ : (x ^ s)⁻¹ - (↑n : ℝ) / (x ^ s * x) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₁₀ : (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹ = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1)))
have hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1)))
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: apply IntervalIntegrable.const_mul
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1)))
have hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1)))
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hf : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hf : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hf₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hg : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hg : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hg₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1))) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -s ≠ -1
have linarith : -s = -1 → 1 - s + -(-s - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -(s + 1) ≠ -1
have linarith : -(s + 1) = -1 → -1 + (1 - s) + -(-(s + 1) - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1))) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have rw : (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) -
    (↑n : ℝ) *
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s + 1) + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + 1) + 1)) / (-(s + 1) + 1)) =
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) -
      (↑n : ℝ) *
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s + 1) + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + 1) + 1)) /
          (-(s + 1) + 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have e_a : (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) -
      (↑n : ℝ) *
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s + 1) + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + 1) + 1)) /
          (-(s + 1) + 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have e_a₁ : (↑n : ℝ) *
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s + 1) + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + 1) + 1)) / (-(s + 1) + 1)) =
  (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a : (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₁ : -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₁ :
  -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₂ : -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₁ :
  -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₂ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₃ : -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
  (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) * (1 / (s - 1))
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₁ :
  -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₂ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₃ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) * (1 / (s - 1))
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₄ : -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
  (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₁ :
  -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₂ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₃ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) * (1 / (s - 1))
e_a₄ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₅ : (HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1)) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1))) / (s - 1) =
  (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₁ :
  -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₂ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₃ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) * (1 / (s - 1))
e_a₄ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
e_a₅ :
  (HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1)) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₆ : ((HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1))⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1))) / (s - 1) =
  (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
this : 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / -(s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₁ :
  -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1)) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₂ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
e_a₃ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) * (1 / (s - 1))
e_a₄ :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1)) - HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
e_a₅ :
  (HPow.hPow (α := ℝ) (↑n : ℝ) (-(s - 1)) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
e_a₆ :
  ((HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1))⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1))) / (s - 1) =
    (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s + 1) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s + 1)) / (-s + 1) =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1))
have e_a₇ : ((HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1))⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-(s - 1))) / (s - 1) =
  ((HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1))⁻¹ - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) / (s - 1)
Tactic: rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]