Theorem: Usa1992P1.digits_pow (Compfiles/Usa1992P1.lean)

State before:
m : ℕ
⊢ (Nat.digits 10 (10 ^ m)).length = m + 1
Tactic:
induction' m with m ih
State after:
case zero

⊢ (Nat.digits 10 (10 ^ 0)).length = 0 + 1

case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ (m + 1))).length = m + 1 + 1

State before:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ (m + 1))).length = m + 1 + 1
Tactic:
rw [pow_succ]
State after:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m * 10)).length = m + 1 + 1

State before:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m * 10)).length = m + 1 + 1
Tactic:
rw [Nat.digits_def' (by norm_num) (by positivity)]
State after:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (10 ^ m * 10 % 10 :: Nat.digits 10 (10 ^ m * 10 / 10)).length = m + 1 + 1

State before:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (10 ^ m * 10 % 10 :: Nat.digits 10 (10 ^ m * 10 / 10)).length = m + 1 + 1
Tactic:
rw [mul_div_cancel_right₀ _ (by norm_num), List.length_cons]
State after:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m)).length.succ = m + 1 + 1

State before:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m)).length.succ = m + 1 + 1
Tactic:
rw [ih]
State after:
no goals

State before:
case zero

⊢ (Nat.digits 10 (10 ^ 0)).length = 0 + 1
Tactic:
simp
State after:
no goals

State before:
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ 1 < 10
Tactic:
norm_num
State after:
no goals

State before:
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ 0 < 10 ^ m * 10
Tactic:
positivity
State after:
no goals

State before:
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ 10 ≠ 0
Tactic:
norm_num
State after:
no goals