calc _ = ∫ x in (1)..↑(n+1), x⁻¹ := ?_
     _ = ∫ x in (1:ℕ)..↑(n+1), x⁻¹ := ?_
     _ ≤ _ := ?_
n : ℕ
⊢ (↑(n + 1)).log ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹

case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹ = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹

case calc_3
n : ℕ
⊢ ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹