Theorem: ZerosOnesAndTwos.factor_ten_pow (Compfiles/ZeroesOnesAndTwos.lean)

State before:
k : ℕ
⊢ 10 ^ k = 2 ^ k * 5 ^ k
Tactic:
induction' k with k' ih
State after:
case zero

⊢ 10 ^ 0 = 2 ^ 0 * 5 ^ 0

case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 10 ^ (k' + 1) = 2 ^ (k' + 1) * 5 ^ (k' + 1)

State before:
case zero

⊢ 10 ^ 0 = 2 ^ 0 * 5 ^ 0
Tactic:
simp only [pow_zero, mul_one]
State after:
no goals

State before:
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 10 ^ (k' + 1) = 2 ^ (k' + 1) * 5 ^ (k' + 1)
Tactic:
rw [pow_succ, pow_succ, pow_succ, ih]
State after:
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 2 ^ k' * 5 ^ k' * 10 = 2 ^ k' * 2 * (5 ^ k' * 5)

State before:
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 2 ^ k' * 5 ^ k' * 10 = 2 ^ k' * 2 * (5 ^ k' * 5)
Tactic:
ring
State after:
no goals