have hx_pos : 0 < x := by
  linarith
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) ≤ (1 + x.log) ^ k
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) ≤ (1 + x.log) ^ k