intro i _
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
a✝ : i ∈ univ
⊢ 0 ≤ (↑(a i))⁻¹