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
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)
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)
⊢ (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]
-- 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)
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)
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)
⊢ (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))⁻¹ - (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)
⊢ (↑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)
have e_a : (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
  (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
⊢ (↑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)
have e_a₁ : (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
  (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
⊢ (↑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)
have e_a₂ : (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
  (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
⊢ (↑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)
have e_a₃ : (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
  (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₃ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
⊢ (↑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)
have e_a₄ : (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
  (↑n : ℝ) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₃ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₄ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s
⊢ (↑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)
have e_a₅ : (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
  (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₃ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₄ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s
e_a₅ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
⊢ (↑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)
have e_a₆ : (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
  (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₃ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₄ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s
e_a₅ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
e_a₆ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
⊢ (↑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)
have e_a₇ : (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₃ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₄ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s
e_a₅ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
e_a₆ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
e_a₇ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
⊢ (↑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)
have e_a₈ : (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)⁻¹) / s) =
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, 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 :
  (↑n : ℝ) * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / -s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₁ :
  (↑n : ℝ) * -((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₂ :
  (↑n : ℝ) * (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s) - HPow.hPow (α := ℝ) (↑n : ℝ) (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₃ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
e_a₄ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s
e_a₅ :
  (↑n : ℝ) * ((HPow.hPow (α := ℝ) (↑n : ℝ) (-s) - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
e_a₆ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * ((1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
e_a₇ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-s)) / s) =
    (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
e_a₈ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)⁻¹) / s) =
    (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) / s)
⊢ (↑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)
have e_a₉ : (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)⁻¹) / s) =
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)⁻¹) / s)
Tactic: rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]