awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
simp_rw :
  ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) / HPow.hPow (β := ℕ) x 2 =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)

Tactic:
simp_rw [← mul_one_div (n : ℝ)]

Premises used: Nat.cast, mul_one_div
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
rw :
  HSub.hSub (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x)
      (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
hf : IntervalIntegrable (HDiv.hDiv (α := ℝ) 1) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
hg :
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) volume (↑n : ℝ)
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)

Tactic:
rw [intervalIntegral.integral_sub]

Premises used: intervalIntegral.integral_sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ HSub.hSub (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x)
      (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)

Tactic:
simp_rw [intervalIntegral.integral_const_mul]

Premises used: intervalIntegral.integral_const_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x) (uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv (α := ℝ) 1) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)

Premises used: LT.lt.ne', intervalIntegral.intervalIntegrable_one_div
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) volume (↑n : ℝ)
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _

Premises used: sq_pos_of_pos, LT.lt.ne', intervalIntegral.intervalIntegrable_one_div, IntervalIntegrable.const_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a : ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)
⊢ (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0
e_a₁ : Ne (α := ℝ) (↑n : ℝ) 0
e_a₂ : LT.lt (α := ℝ) 0 (↑n : ℝ)
e_a₃ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)

Tactic:
rw [integral_one_div_of_pos, log_div]

Premises used: Real.log_div, integral_one_div_of_pos
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))

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

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a :
  ∀ (x : ℝ) (hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    1 / HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℝ) x (-2)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))

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

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
e_a : 0 ≤ x
⊢ 1 / HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℝ) x (-2)

Tactic:
rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]

Premises used: one_div, Real.rpow_neg, Nat.cast_two, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ x

Tactic:
(hv x hx).le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ x

Tactic:
exact (hv x hx).le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
rw :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HAdd.hAdd (α := ℝ) (-2) 1 -
            HPow.hPow (α := ℝ) (↑n : ℝ) (HAdd.hAdd (α := ℝ) (-2) 1)) /
          HAdd.hAdd (α := ℝ) (-2) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₁ : LT.lt (α := ℝ) (-1) (-2) ∨ Ne (α := ℝ) (-2) (-1) ∧ 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2)) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
rw [integral_rpow]

Premises used: integral_rpow
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ HAdd.hAdd (α := ℝ) (-2) 1 = -1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
simp_rw :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HAdd.hAdd (α := ℝ) (-2) 1 / HAdd.hAdd (α := ℝ) (-2) 1 -
          HPow.hPow (α := ℝ) (↑n : ℝ) (HAdd.hAdd (α := ℝ) (-2) 1) / HAdd.hAdd (α := ℝ) (-2) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
simp_rw₁ :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        (HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-1) / -1 -
          HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) / -1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
simp_rw₂ :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        (-(HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-1) / 1) -
          -(HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) / 1)) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
simp_rw₃ :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        (-HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-1) - -HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
simp_rw₄ :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) - HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-1)) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
simp_rw₅ :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - (↑n : ℝ) * ((↑n : ℝ)⁻¹ - (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HAdd.hAdd (α := ℝ) (-2) 1 -
            HPow.hPow (α := ℝ) (↑n : ℝ) (HAdd.hAdd (α := ℝ) (-2) 1)) /
          HAdd.hAdd (α := ℝ) (-2) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]

Premises used: Real.rpow_neg_one, sub_div, div_neg, one_div, neg_sub_neg, div_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ Ne (α := ℝ) (-2) (-1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
refine_1 : LT.lt (α := ℝ) 0 (↑n : ℝ)
refine_2 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ LT.lt (α := ℝ) (-1) (-2) ∨ Ne (α := ℝ) (-2) (-1) ∧ 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a : (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₅ : 0 = log 1 - (↑(↑1 : ℚ)⁻¹ : ℝ) + 1
zero₆ : 0 = log 1 - (↑1⁻¹ : ℝ) + 1
zero₇ : 0 = log 1 - (↑1 : ℝ) + 1
zero₈ : 0 = log 1 - 1 + 1
zero₉ : 0 = HSub.hSub (α := ℝ) 0 1 + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1

Tactic:
simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]

Premises used: inv_one, ZetaAsymptotics.term_sum, harmonic_zero, Real.log_one, Finset.sum_range_zero, zero_add, harmonic_succ, Nat.cast_zero, sub_add_cancel, Nat.cast_one, Rat.cast_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
⊢ 0 < N + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
succ :
  log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
      (log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - log (↑(N + 1) : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1) + (↑(N + 1 + 1) : ℚ)⁻¹) : ℝ) + 1
⊢ ∑ n ∈ Finset.range (N + 1), term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1 + 1)) : ℝ) + 1

Tactic:
rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
      term_one (by positivity : 0 < N + 1)]

Premises used: ZetaAsymptotics.term_one, harmonic_succ, HAdd.hAdd, OfNat.ofNat, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
succ :
  log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
      (log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) - log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) -
        1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1)) =
    log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) - ((↑(harmonic (N + 1)) : ℝ) + (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1)⁻¹) + 1
⊢ log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
      (log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - log (↑(N + 1) : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1) + (↑(N + 1 + 1) : ℚ)⁻¹) : ℝ) + 1

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
⊢ log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
      (log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) - log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) -
        1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1)) =
    log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) - ((↑(harmonic (N + 1)) : ℝ) + (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1)⁻¹) + 1

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
zero : term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
succ :
  ∀ (N : ℕ) (hN : term_sum 1 N = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1),
    term_sum 1 (N + 1) = log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1 + 1)) : ℝ) + 1
⊢ term_sum 1 N = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1

Tactic:
induction N with
  | zero =>
    simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
  | succ N hN =>
    unfold term_sum at hN ⊢
    rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
      term_one (by positivity : 0 < N + 1)]
    push_cast
    ring_nf

Premises used: inv_one, ZetaAsymptotics.term_sum, harmonic_zero, Real.log_one, Finset.sum_range_zero, ZetaAsymptotics.term_one, zero_add, harmonic_succ, HAdd.hAdd, Nat.cast_zero, OfNat.ofNat, sub_add_cancel, Nat.cast_one, Finset.sum_range_succ, Rat.cast_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))
⊢ HasSum (fun (n : ℕ) ↦ term (n + 1) 1) (1 - γ)

Tactic:
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) 1)]

Premises used: HAdd.hAdd, ZetaAsymptotics.term_nonneg, OfNat.ofNat, hasSum_iff_tendsto_nat_of_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
simp_rw :
  Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) + 1) atTop (𝓝 (-γ + 1))
⊢ Tendsto (fun (N : ℕ) ↦ term_sum 1 N) atTop (𝓝 (1 - γ))

Tactic:
simp_rw [term_sum_one, sub_eq_neg_add]

Premises used: sub_eq_neg_add, ZetaAsymptotics.term_sum_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) + 1) atTop (𝓝 (-γ + 1))

Tactic:
Tendsto.add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
refine : Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) atTop (𝓝 (-γ))
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) + 1) atTop (𝓝 (-γ + 1))

Tactic:
refine Tendsto.add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))

Tactic:
have := (tendsto_eulerMascheroniSeq'.comp (tendsto_add_atTop_nat 1)).neg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) atTop (𝓝 (-γ))

Tactic:
this.congr' (Eventually.of_forall (fun n ↦ ?_))

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
refine :
  ∀ (n : ℕ),
    -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) n =
      (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) n
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) atTop (𝓝 (-γ))

Tactic:
refine this.congr' (Eventually.of_forall (fun n ↦ ?_))

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
push_cast :
  -((↑(harmonic (n + 1)) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) =
    -(↑(harmonic (n + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -((↑(harmonic (n + 1)) : ℝ) - log (↑(n + 1) : ℝ)) = -(↑(harmonic (n + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -((↑(harmonic (n + 1)) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) =
    -(↑(harmonic (n + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
abel
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

Premises used: le_add_iff_nonneg_right, zero_le_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx

Premises used: Set.uIcc_of_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 < x

Tactic:
(Nat.cast_pos.mpr hn).trans_le hx.1

Premises used: Iff.mpr, Nat.cast_pos, And.left, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 < x

Tactic:
exact (Nat.cast_pos.mpr hn).trans_le hx.1

Premises used: Iff.mpr, Nat.cast_pos, And.left, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
⊢ ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x

Tactic:
have hv : ∀ x ∈ uIcc (n : ℝ) (n + 1), 0 < x := by
    intro x hx
    rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
    exact (Nat.cast_pos.mpr hn).trans_le hx.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
⊢ term n s = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ 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:
intervalIntegral.integral_congr (fun x hx ↦ ?_)

Premises used: intervalIntegral.integral_congr