calc
  ∑ d : ℕ in Ico 2 (n + 1), (d : ℝ)⁻¹ = ∑ d in Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
  _ ≤ ∫ x in (2).. ↑(n + 1), (x - 1)⁻¹  := ?_
  _ = Real.log ↑n := ?_
case h₂
n : ℕ
hn : 1 ≤ n
⊢ ∑ x ∈ Ioc 1 n, (↑x)⁻¹ ≤ (↑n).log
case h₂.calc_1
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Ico 2 (n + 1), (↑d)⁻¹ = ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹

case h₂.calc_2
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ ≤ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹

case h₂.calc_3
n : ℕ
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 2 ..↑(n + 1), (x - 1)⁻¹ = (↑n).log