awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ 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)
have 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)
Tactic: simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ LT.lt (α := ℝ) (-1) (-2) ∨ Ne (α := ℝ) (-2) (-1) ∧ 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have refine_1 : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
refine_1 : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ LT.lt (α := ℝ) (-1) (-2) ∨ Ne (α := ℝ) (-2) (-1) ∧ 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have refine_2 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ 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
have e_a : (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ term n 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have calc : term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
Tactic: calc term n 1
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ 2 := by
      simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
    _ = ∫ x : ℝ in n..(n + 1), (1 / x - n / x ^ 2) :=
      intervalIntegral.integral_congr (fun x hx ↦ by field)
    _ = (∫ x : ℝ in n..(n + 1), 1 / x) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      simp_rw [← mul_one_div (n : ℝ)]
      rw [intervalIntegral.integral_sub]
      · simp_rw [intervalIntegral.integral_const_mul]
      · exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)
      · exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      congr 1
      rw [integral_one_div_of_pos, log_div]
      all_goals positivity
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), x ^ (-2 : ℝ) := by
      congr 2
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
      exact (hv x hx).le
    _ = log (↑n + 1) - log ↑n - n * (1 / n - 1 / (n + 1)) := by
      rw [integral_rpow]
      · simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
      · refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity
    _ = log (↑n + 1) - log ↑n - 1 / (↑n + 1) := by
      congr 1
      simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
⊢ term n 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have calc₁ : ∫ (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: calc term n 1
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ 2 := by
      simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
    _ = ∫ x : ℝ in n..(n + 1), (1 / x - n / x ^ 2) :=
      intervalIntegral.integral_congr (fun x hx ↦ by field)
    _ = (∫ x : ℝ in n..(n + 1), 1 / x) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      simp_rw [← mul_one_div (n : ℝ)]
      rw [intervalIntegral.integral_sub]
      · simp_rw [intervalIntegral.integral_const_mul]
      · exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)
      · exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      congr 1
      rw [integral_one_div_of_pos, log_div]
      all_goals positivity
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), x ^ (-2 : ℝ) := by
      congr 2
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
      exact (hv x hx).le
    _ = log (↑n + 1) - log ↑n - n * (1 / n - 1 / (n + 1)) := by
      rw [integral_rpow]
      · simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
      · refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity
    _ = log (↑n + 1) - log ↑n - 1 / (↑n + 1) := by
      congr 1
      simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
calc₁ :
  ∫ (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)
⊢ term n 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have calc₂ : (∫ (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: calc term n 1
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ 2 := by
      simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
    _ = ∫ x : ℝ in n..(n + 1), (1 / x - n / x ^ 2) :=
      intervalIntegral.integral_congr (fun x hx ↦ by field)
    _ = (∫ x : ℝ in n..(n + 1), 1 / x) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      simp_rw [← mul_one_div (n : ℝ)]
      rw [intervalIntegral.integral_sub]
      · simp_rw [intervalIntegral.integral_const_mul]
      · exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)
      · exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      congr 1
      rw [integral_one_div_of_pos, log_div]
      all_goals positivity
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), x ^ (-2 : ℝ) := by
      congr 2
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
      exact (hv x hx).le
    _ = log (↑n + 1) - log ↑n - n * (1 / n - 1 / (n + 1)) := by
      rw [integral_rpow]
      · simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
      · refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity
    _ = log (↑n + 1) - log ↑n - 1 / (↑n + 1) := by
      congr 1
      simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
calc₁ :
  ∫ (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)
calc₂ :
  (∫ (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)
⊢ term n 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have calc₃ : 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: calc term n 1
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ 2 := by
      simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
    _ = ∫ x : ℝ in n..(n + 1), (1 / x - n / x ^ 2) :=
      intervalIntegral.integral_congr (fun x hx ↦ by field)
    _ = (∫ x : ℝ in n..(n + 1), 1 / x) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      simp_rw [← mul_one_div (n : ℝ)]
      rw [intervalIntegral.integral_sub]
      · simp_rw [intervalIntegral.integral_const_mul]
      · exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)
      · exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      congr 1
      rw [integral_one_div_of_pos, log_div]
      all_goals positivity
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), x ^ (-2 : ℝ) := by
      congr 2
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
      exact (hv x hx).le
    _ = log (↑n + 1) - log ↑n - n * (1 / n - 1 / (n + 1)) := by
      rw [integral_rpow]
      · simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
      · refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity
    _ = log (↑n + 1) - log ↑n - 1 / (↑n + 1) := by
      congr 1
      simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero : ∑ n ∈ Finset.range 0, term (n + 1) 1 =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₁ : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
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
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(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]