rw [intervalIntegral.integral_comp_sub_right _ 1, integral_inv]
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹ = (↑n).log
case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ((↑(n + 1) - 1) / (2 - 1)).log = (↑n).log

case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc (2 - 1) (↑(n + 1) - 1)