gcongr with i hi
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ ∑ a ∈ filter (fun a => ↑a ≤ x) P.divisors, ↑h ^ ω a ≤ ∑ a ∈ filter (fun a => ↑a ≤ x) P.divisors, x * (↑h ^ ω a / ↑a)
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ x * (↑h ^ ω i / ↑i)