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