case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ ↑(ppow f (k + 1)) x = ↑(pmul (ppow f k) f) x
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
⊢ ppow f (k + 1) = pmul (ppow f k) f
ext x
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ ↑f x * ↑f x ^ k = ↑(pmul (ppow f k) f) x
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ ↑(ppow f (k + 1)) x = ↑(pmul (ppow f k) f) x
rw [ppow_apply (Nat.succ_pos k), pow_succ'']
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ∀ {kpos : 0 < n✝}, ↑f x * ↑f x ^ n✝ = ↑(pmul (ppow f n✝) f) x
kpos : 0 < succ n✝
⊢ ↑f x * ↑f x ^ succ n✝ = ↑f x ^ succ n✝ * ↑f x
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ ↑f x * ↑f x ^ k = ↑(pmul (ppow f k) f) x
induction k <;> simp
no goals
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ∀ {kpos : 0 < n✝}, ↑f x * ↑f x ^ n✝ = ↑(pmul (ppow f n✝) f) x
kpos : 0 < succ n✝
⊢ ↑f x * ↑f x ^ succ n✝ = ↑f x ^ succ n✝ * ↑f x
rw [pow_mul_comm']