calc _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
     _ ≤ _ := ?_
y : ℝ
hy : 1 ≤ y
⊢ y.log ≤ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹
case calc_1
y : ℝ
hy : 1 ≤ y
⊢ y.log ≤ (↑(⌊y⌋₊ + 1)).log

case calc_2
y : ℝ
hy : 1 ≤ y
⊢ (↑(⌊y⌋₊ + 1)).log ≤ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹