rw [←mul_sum]
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0) ≤ x * (1 + x.log) ^ h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (x * ∑ i ∈ P.divisors, if ↑i ≤ x then ↑h ^ ω i / ↑i else 0) ≤ x * (1 + x.log) ^ h