case h
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑↑f x✝ = ↑↑f x✝
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
⊢ ↑↑f = ↑f
ext
no goals
case h
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑↑f x✝ = ↑↑f x✝
simp