case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ ↑(ppow f (k + 1)) x = ↑(pmul f (ppow f k)) x
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
⊢ ppow f (k + 1) = pmul f (ppow f k)
ext x
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ ↑f x ^ succ k = ↑(pmul f (ppow f k)) x
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ ↑(ppow f (k + 1)) x = ↑(pmul f (ppow f k)) x
simp_rw [ppow_apply (Nat.succ_pos k), pow_succ]
case h.zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑f x ^ succ 0 = ↑f x

case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ↑f x ^ succ n✝ = ↑(pmul f (ppow f n✝)) x
⊢ ↑f x ^ succ (succ n✝) = ↑f x * ↑f x ^ succ n✝
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ ↑f x ^ succ k = ↑(pmul f (ppow f k)) x
induction k <;> simp
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ↑f x ^ succ n✝ = ↑(pmul f (ppow f n✝)) x
⊢ ↑f x ^ succ (succ n✝) = ↑f x * ↑f x ^ succ n✝
case h.zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑f x ^ succ 0 = ↑f x

case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ↑f x ^ succ n✝ = ↑(pmul f (ppow f n✝)) x
⊢ ↑f x ^ succ (succ n✝) = ↑f x * ↑f x ^ succ n✝
. exact pow_one _
no goals
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ↑f x ^ succ n✝ = ↑(pmul f (ppow f n✝)) x
⊢ ↑f x ^ succ (succ n✝) = ↑f x * ↑f x ^ succ n✝
. exact pow_succ'' _ _
no goals
case h.zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑f x ^ succ 0 = ↑f x
exact pow_one _
no goals
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ↑f x ^ succ n✝ = ↑(pmul f (ppow f n✝)) x
⊢ ↑f x ^ succ (succ n✝) = ↑f x * ↑f x ^ succ n✝
exact pow_succ'' _ _