case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(pmul f g) x✝ = ↑(pmul g f) x✝
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ pmul f g = pmul g f
ext
no goals
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(pmul f g) x✝ = ↑(pmul g f) x✝
simp [mul_comm]