simp_rw [pmul_apply, hf.2, hg.2]
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b * (g a * g b) = f a * g a * (f b * g b)