rw [←div_eq_mul_inv]
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x * (↑i)⁻¹
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x / ↑i