-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
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))
calc₄ :
  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)
calc₅ :
  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
⊢ term n 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

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]

Premises used: intervalIntegral.integral_congr, HSub.hSub, intervalIntegral, HDiv.hDiv, Nat.cast, Real.log, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, ZetaAsymptotics.term, OfNat.ofNat, Neg.neg