simp_rw [hf.apply_pow]
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f p ^ n = ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n)
no goals