rw [hf.isMultiplicative.map_prod_of_subset_primeFactors _ _ subset_rfl,
  ←Finset.prod_mul_distrib]
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
⊢ f (∏ p ∈ d.primeFactors, p) * ∏ p ∈ d.primeFactors, 1 / (1 - f p) = ∏ p ∈ d.primeFactors, f p / (1 - f p)
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
⊢ ∏ x ∈ d.primeFactors, f x * (1 / (1 - f x)) = ∏ p ∈ d.primeFactors, f p / (1 - f p)