rw [Fintype.mem_piFinset] at ha
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x