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

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

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

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
have h3 : (Nat.digits 10 y).length ≤ m := by
  have h4 := lemma2 h1
  exact Nat.le_of_lt_succ h4
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
have ⟨k, hk⟩ : ∃ k, k + (Nat.digits 10 y).length = m := by
  obtain ⟨k, hk⟩ := Nat.le.dest h3
  rw [add_comm] at hk
  exact ⟨k, hk⟩
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
nth_rewrite 1 [add_comm, mul_comm]
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 (y + 10 ^ m * (x + 1))).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 (y + 10 ^ m * (x + 1))).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
nth_rewrite 1 [←hk]
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
have one_lt_ten : 1 < 10 := by norm_num
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
have h5 := @digits_append_zeroes_append_digits 10 k _ y (Nat.zero_lt_succ x) one_lt_ten
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
rw [←h5]
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
simp only [List.sum_append]
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (List.replicate k 0).sum + (Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (List.replicate k 0).sum + (Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
simp only [List.sum_replicate, smul_eq_mul, mul_zero, add_zero]
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
rw [digits_sum_mul_pow]
State after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 (x + 1)).sum + (Nat.digits 10 y).sum

State before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 (x + 1)).sum + (Nat.digits 10 y).sum
Tactic:
ring
State after:
no goals

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

State before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
⊢ (Nat.digits 10 y).length ≤ m
Tactic:
have h4 := lemma2 h1
State after:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h4 : (Nat.digits 10 y).length < m + 1
⊢ (Nat.digits 10 y).length ≤ m

State before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h4 : (Nat.digits 10 y).length < m + 1
⊢ (Nat.digits 10 y).length ≤ m
Tactic:
exact Nat.le_of_lt_succ h4
State after:
no goals

State before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest h3
State after:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : (Nat.digits 10 y).length + k = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m

State before:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : (Nat.digits 10 y).length + k = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Tactic:
rw [add_comm] at hk
State after:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m

State before:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Tactic:
exact ⟨k, hk⟩
State after:
no goals

State before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ 1 < 10
Tactic:
norm_num
State after:
no goals