rw [div_eq_mul_inv, mul_comm _ (i:ℝ)⁻¹, ←mul_assoc]
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)
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ x * (↑i)⁻¹ * ↑h ^ ω i