rw [←prod_erase_mul (a:=i) (h:= hi)]
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
⊢ a i ≤ ∏ i : Fin k, a i
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
⊢ a i ≤ (∏ x ∈ univ.erase i, a x) * a i