rw [← Finset.sum_erase_add (Icc 1 n) _ (by simp [hn] : 1 ∈ Icc 1 n), add_comm]
n : ℕ
hn : 1 ≤ n
⊢ ∑ d ∈ Icc 1 n, (↑d)⁻¹ ≤ 1 + (↑n).log
n : ℕ
hn : 1 ≤ n
⊢ (↑1)⁻¹ + ∑ x ∈ (Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + (↑n).log