Theorem: Sieve.CompletelyMultiplicative.apply_pow (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
a n : ℕ
⊢ f (a ^ n) = f a ^ n
Tactic:
induction n with
| zero => simp_rw [pow_zero, hf.1]
| succ n' ih => simp_rw [pow_succ, hf.2, ih]
State after:
no goals

State before:
case zero
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
a : ℕ
⊢ f (a ^ 0) = f a ^ 0
Tactic:
simp_rw [pow_zero, hf.1]
State after:
no goals

State before:
case succ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
a n' : ℕ
ih : f (a ^ n') = f a ^ n'
⊢ f (a ^ (n' + 1)) = f a ^ (n' + 1)
Tactic:
simp_rw [pow_succ, hf.2, ih]
State after:
no goals