rw [Finset.prod_sum]
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
⊢ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n) = ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m