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

State before:
m x : ℕ
⊢ (Nat.digits 10 (x * 10 ^ m)).sum = (Nat.digits 10 x).sum
Tactic:
cases' x with x
State after:
case zero
m : ℕ
⊢ (Nat.digits 10 (0 * 10 ^ m)).sum = (Nat.digits 10 0).sum

case succ
m x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum

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

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

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

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

State before:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ ((x + 1) * (10 ^ m * 10) % 10 :: Nat.digits 10 ((x + 1) * (10 ^ m * 10) / 10)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
rw [←mul_assoc, Nat.mul_mod, Nat.mod_self, mul_zero, Nat.zero_mod]
State after:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (0 :: Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum

State before:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (0 :: Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
rw [List.sum_cons, zero_add]
State after:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum

State before:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
have h10 : 10 ≠ 0 := by norm_num
State after:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
h10 : 10 ≠ 0
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum

State before:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
h10 : 10 ≠ 0
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
rw [mul_div_cancel_right₀ _ h10]
State after:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
h10 : 10 ≠ 0
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum

State before:
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
h10 : 10 ≠ 0
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
exact ih
State after:
no goals

State before:
case zero
m : ℕ
⊢ (Nat.digits 10 (0 * 10 ^ m)).sum = (Nat.digits 10 0).sum
Tactic:
simp
State after:
no goals

State before:
case succ.zero
x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ 0)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
simp
State after:
no goals

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

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

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