awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
refine :
  ∀ (x : ℝ) (hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)))

Tactic:
refine intervalIntegral.integral_congr (fun x hx ↦ ?_)

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)⁻¹
rw₁₀ rw₁₁ : (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹ = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))

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]

Premises used: LT.lt.le, sub_div, div_eq_mul_inv, Real.rpow_add_one, LT.lt.ne', one_div, mul_comm, div_div, Real.rpow_neg, div_self
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
hg :
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (-(s + 1))) 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)))

Tactic:
rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul]

Premises used: intervalIntegral.integral_sub, intervalIntegral.integral_const_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) 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)))

Tactic:
rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul]

Premises used: intervalIntegral.integral_sub, intervalIntegral.integral_const_mul, IntervalIntegrable.const_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)

Tactic:
intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)

Premises used: Set.notMem_uIcc_of_lt, intervalIntegral.intervalIntegrable_rpow, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hf : LT.lt (α := ℝ) 0 (↑n : ℝ)
hf₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-s)) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)

Premises used: Set.notMem_uIcc_of_lt, intervalIntegral.intervalIntegrable_rpow, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
exact_mod_cast hn
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)

Tactic:
intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)

Premises used: Set.notMem_uIcc_of_lt, intervalIntegral.intervalIntegrable_rpow, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
hg : LT.lt (α := ℝ) 0 (↑n : ℝ)
hg₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(s + 1))) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)

Premises used: Set.notMem_uIcc_of_lt, intervalIntegral.intervalIntegrable_rpow, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
linarith : -s = -1 → 1 - s + -(-s - -1) = 0
⊢ -s ≠ -1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
linarith : -(s + 1) = -1 → -1 + (1 - s) + -(-(s + 1) - -1) = 0
⊢ -(s + 1) ≠ -1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
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)
⊢ (∫ (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)

Tactic:
rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]

Premises used: integral_rpow, And.intro, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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₁ :
  (↑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)
⊢ (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:
congr 1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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 = -(s - 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
e_a₉ 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)
⊢ (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]

Premises used: neg_sub, neg_div, Nat.cast_nonneg, mul_one_div, div_neg, one_div, mul_comm, Real.rpow_neg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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 = -s

Tactic:
ring
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
e_a₉ e_a₁₀ :
  (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)⁻¹) / s) =
    (↑n : ℝ) * (((HPow.hPow (α := ℝ) (↑n : ℝ) s)⁻¹ - (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)

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]

Premises used: neg_sub, neg_div, Nat.cast_nonneg, mul_div_assoc, div_mul_eq_mul_div, div_neg, one_div, Real.rpow_neg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n s = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1)
calc₁ :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)))
calc₂ :
  ∫ (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)))
calc₃ :
  (∫ (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)
⊢ term n s =
    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:
calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      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]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · 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]
      · 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]

Premises used: HSub.hSub, intervalIntegral, Nat.cast, HPow.hPow, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, ZetaAsymptotics.term, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
h : ∀ (n : ℕ), term (n + 1) s
| ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)

Tactic:
enter [1, 2, n]
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 < n + 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
h :
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
    (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)
| term (n + 1) s

Tactic:
rw [term_of_lt (by simp) hs]

Premises used: ZetaAsymptotics.term_of_lt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
h :
  ∀ (n : ℕ),
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
      (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)
| ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)

Tactic:
enter [1, 2, n]; rw [term_of_lt (by simp) hs]

Premises used: ZetaAsymptotics.term_of_lt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
conv :
  ∑ n ∈ Finset.range N,
      (1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
        (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
⊢ ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)

Tactic:
conv => enter [1, 2, n]; rw [term_of_lt (by simp) hs]

Premises used: ZetaAsymptotics.term_of_lt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
rw :
  HSub.hSub (α := ℝ)
      (∑ x ∈ Finset.range N,
        1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)))
      (∑ x ∈ Finset.range N,
        (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
⊢ ∑ n ∈ Finset.range N,
      (1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
        (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)

Tactic:
rw [Finset.sum_sub_distrib]

Premises used: Finset.sum_sub_distrib
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
e_a₁ :
  ∑ x ∈ Finset.range N,
      (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
⊢ HSub.hSub (α := ℝ)
      (∑ x ∈ Finset.range N,
        1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)))
      (∑ x ∈ Finset.range N,
        (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)

Tactic:
congr 1