trans (∑ d in Icc 1 (floor x), (d:ℝ)⁻¹)
case calc_5.hab
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ 1 + x.log
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹ ≤ 1 + x.log