-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_one {n : ℕ} (hn : 0 < n) :
    term n 1 = (log (n + 1) - log n) -  1 / (n + 1)

Proof state:
case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 1 / x ^ 2 = x ^ (-2)

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

Result:
case e_a.e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ x

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1)) = log (↑n + 1) - log ↑n - 1 / (↑n + 1)

Tactic:
congr 1

Result:
case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n * (1 / ↑n - 1 / (↑n + 1)) = 1 / (↑n + 1)

Proof state:
case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2 = ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2)

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

Result:
case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 1 / x ^ 2 = x ^ (-2)

Proof state:
case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n * (1 / ↑n - 1 / (↑n + 1)) = 1 / (↑n + 1)

Tactic:
field_simp

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ContinuousOn (fun x => x) (uIcc (↑n) (↑n + 1))

Tactic:
fun_prop

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n / x ^ 2 =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

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

Result:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ∫ (x : ℝ) in ↑n..↑n + 1, ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Tactic:
simp_rw [intervalIntegral.integral_const_mul]

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -2 ≠ -1

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_2
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
positivity

Result:
no goals

Proof state:
case e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n + 1 ≠ 0

case e_a.hy
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n ≠ 0

case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
all_goals positivity

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -1 < -2 ∨ -2 ≠ -1 ∧ 0 ∉ uIcc (↑n) (↑n + 1)

Tactic:
refine Or.inr ⟨by norm_num, not_mem_uIcc_of_lt ?_ ?_⟩

Result:
case refine_1
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case refine_2
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Proof state:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ ↑n ≤ ↑n + 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 < x

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

Result:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 < x

Proof state:
case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Tactic:
rw [intervalIntegral.integral_sub]

Result:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ∫ (x : ℝ) in ↑n..↑n + 1, ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

case hf
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv 1) volume (↑n) (↑n + 1)

case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x => ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ 2 = ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n / x ^ 2

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

Result:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x - ↑n) / x ^ 2 = 1 / x - ↑n / x ^ 2

Proof state:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 < x

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

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
⊢ term n 1 = log (↑n + 1) - log ↑n - 1 / (↑n + 1)

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

Result:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ term n 1 = log (↑n + 1) - log ↑n - 1 / (↑n + 1)

Proof state:
case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x = log (↑n + 1) - log ↑n

Tactic:
rw [integral_one_div_of_pos, log_div]

Result:
case e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n + 1 ≠ 0

case e_a.hy
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n ≠ 0

case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ term n 1 = ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ 2

Tactic:
simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]

Result:
no goals

Proof state:
case e_a.e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ x

Tactic:
exact (hv x hx).le

Result:
no goals

Proof state:
case hf
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv 1) volume (↑n) (↑n + 1)

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

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x

Tactic:
intro x hx

Result:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 < x

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x - ↑n) / x ^ 2 = 1 / x - ↑n / x ^ 2

Tactic:
field_simp [(hv x hx).ne']

Result:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x - ↑n) * (x * x ^ 2) = (x ^ 2 - x * ↑n) * x ^ 2

Proof state:
case refine_1
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case refine_2
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
all_goals positivity

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -2 + 1 = -1

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2 =
    log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Tactic:
congr 1

Result:
case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x = log (↑n + 1) - log ↑n

Proof state:
case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x => ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)

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

Result:
no goals