rw [prod_univ_sum]
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors, ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0) =
    ∏ _i : Fin k, ∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0
no goals