internlm/Lean-Github huggingface dataset:
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
b k n : ℕ
hb : 1 < b
⊢ ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
Tactic:
induction' k with k ih
Proof state after:
case zero
b n : ℕ
hb : 1 < b
⊢ ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate 0 0 ++ b.digits m = b.digits (n + b ^ (0 + (b.digits n).length) * m)

case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
⊢ ∀ {m : ℕ},
    0 < m → b.digits n ++ List.replicate (k + 1) 0 ++ b.digits m = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
⊢ ∀ {m : ℕ},
    0 < m → b.digits n ++ List.replicate (k + 1) 0 ++ b.digits m = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
intro m hm
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
⊢ b.digits n ++ List.replicate (k + 1) 0 ++ b.digits m = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
⊢ b.digits n ++ List.replicate (k + 1) 0 ++ b.digits m = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
rw [List.replicate_succ', List.append_assoc, List.append_assoc, List.singleton_append]
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
have hmb : 0 < m * b := lt_mul_of_lt_of_one_lt' hm hb
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
let h1 := digits_def' hb hmb
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
have h2 : m = m * b / b := by
  exact Nat.eq_div_of_mul_eq_left (not_eq_zero_of_lt hb) rfl
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
h2 : m = m * b / b
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
h2 : m = m * b / b
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
simp only [mul_mod_left, ←h2] at h1
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits n ++ (List.replicate k 0 ++ 0 :: b.digits m) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
rw [←h1, ←List.append_assoc, ih hmb]
Proof state after:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits (n + b ^ (k + (b.digits n).length) * (m * b)) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case succ
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits (n + b ^ (k + (b.digits n).length) * (m * b)) = b.digits (n + b ^ (k + 1 + (b.digits n).length) * m)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
case zero
b n : ℕ
hb : 1 < b
⊢ ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate 0 0 ++ b.digits m = b.digits (n + b ^ (0 + (b.digits n).length) * m)
Tactic:
simp [digits_append_digits (zero_lt_of_lt hb)]
Proof state after:
no goals
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
b n : ℕ
hb : 1 < b
k : ℕ
ih :
  ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
⊢ m = m * b / b
Tactic:
exact Nat.eq_div_of_mul_eq_left (not_eq_zero_of_lt hb) rfl
Proof state after:
no goals
Theorem: Usa1992P1.digits_pow
Proof state before:
m : ℕ
⊢ (Nat.digits 10 (10 ^ m)).length = m + 1
Tactic:
induction' m with m ih
Proof 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
Theorem: Usa1992P1.digits_pow
Proof 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]
Proof state after:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m * 10)).length = m + 1 + 1
Theorem: Usa1992P1.digits_pow
Proof 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)]
Proof 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
Theorem: Usa1992P1.digits_pow
Proof 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]
Proof state after:
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m)).length.succ = m + 1 + 1
Theorem: Usa1992P1.digits_pow
Proof 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]
Proof state after:
no goals
Theorem: Usa1992P1.digits_pow
Proof state before:
case zero

⊢ (Nat.digits 10 (10 ^ 0)).length = 0 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.digits_pow
Proof state before:
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ 1 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa1992P1.digits_pow
Proof state before:
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ 0 < 10 ^ m * 10
Tactic:
positivity
Proof state after:
no goals
Theorem: Usa1992P1.digits_pow
Proof state before:
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ 10 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa1992P1.lemma2
Proof state before:
m y : ℕ
hy : y < 10 ^ m
⊢ (Nat.digits 10 y).length < m + 1
Tactic:
revert y
Proof state after:
m : ℕ
⊢ ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
Theorem: Usa1992P1.lemma2
Proof state before:
m : ℕ
⊢ ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
Tactic:
induction' m with m ih
Proof state after:
case zero

⊢ ∀ {y : ℕ}, y < 10 ^ 0 → (Nat.digits 10 y).length < 0 + 1

case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
⊢ ∀ {y : ℕ}, y < 10 ^ (m + 1) → (Nat.digits 10 y).length < m + 1 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
⊢ ∀ {y : ℕ}, y < 10 ^ (m + 1) → (Nat.digits 10 y).length < m + 1 + 1
Tactic:
intro y hy
Proof state after:
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
⊢ (Nat.digits 10 y).length < m + 1 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
⊢ (Nat.digits 10 y).length < m + 1 + 1
Tactic:
obtain rfl | hyp := Nat.eq_zero_or_pos y
Proof state after:
case succ.inl
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
hy : 0 < 10 ^ (m + 1)
⊢ (Nat.digits 10 0).length < m + 1 + 1

case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 y).length < m + 1 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 y).length < m + 1 + 1
Tactic:
rw [Nat.digits_def' (by norm_num) hyp]
Proof state after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (y % 10 :: Nat.digits 10 (y / 10)).length < m + 1 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (y % 10 :: Nat.digits 10 (y / 10)).length < m + 1 + 1
Tactic:
rw [List.length_cons]
Proof state after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length.succ < m + 1 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length.succ < m + 1 + 1
Tactic:
rw [Nat.succ_eq_add_one, add_lt_add_iff_right]
Proof state after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length < m + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length < m + 1
Tactic:
have h2 : y / 10 < 10 ^ m := by omega
Proof state after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
h2 : y / 10 < 10 ^ m
⊢ (Nat.digits 10 (y / 10)).length < m + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
h2 : y / 10 < 10 ^ m
⊢ (Nat.digits 10 (y / 10)).length < m + 1
Tactic:
exact ih h2
Proof state after:
no goals
Theorem: Usa1992P1.lemma2
Proof state before:
case zero

⊢ ∀ {y : ℕ}, y < 10 ^ 0 → (Nat.digits 10 y).length < 0 + 1
Tactic:
intro y hy
Proof state after:
case zero
y : ℕ
hy : y < 10 ^ 0
⊢ (Nat.digits 10 y).length < 0 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case zero
y : ℕ
hy : y < 10 ^ 0
⊢ (Nat.digits 10 y).length < 0 + 1
Tactic:
obtain rfl: y = 0 := by omega
Proof state after:
case zero
hy : 0 < 10 ^ 0
⊢ (Nat.digits 10 0).length < 0 + 1
Theorem: Usa1992P1.lemma2
Proof state before:
case zero
hy : 0 < 10 ^ 0
⊢ (Nat.digits 10 0).length < 0 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.lemma2
Proof state before:
y : ℕ
hy : y < 10 ^ 0
⊢ y = 0
Tactic:
omega
Proof state after:
no goals
Theorem: Usa1992P1.lemma2
Proof state before:
case succ.inl
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
hy : 0 < 10 ^ (m + 1)
⊢ (Nat.digits 10 0).length < m + 1 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.lemma2
Proof state before:
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ 1 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa1992P1.lemma2
Proof state before:
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ y / 10 < 10 ^ m
Tactic:
omega
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum_mul_pow
Proof state before:
m x : ℕ
⊢ (Nat.digits 10 (x * 10 ^ m)).sum = (Nat.digits 10 x).sum
Tactic:
cases' x with x
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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]
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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)]
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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]
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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]
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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]
Proof 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
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum_mul_pow
Proof state before:
case zero
m : ℕ
⊢ (Nat.digits 10 (0 * 10 ^ m)).sum = (Nat.digits 10 0).sum
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum_mul_pow
Proof state before:
case succ.zero
x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ 0)).sum = (Nat.digits 10 (x + 1)).sum
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum_mul_pow
Proof state before:
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ 1 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum_mul_pow
Proof 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
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum_mul_pow
Proof state before:
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ 10 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum
Proof 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
Proof 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
Theorem: Usa1992P1.digits_sum
Proof 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
Proof 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
Theorem: Usa1992P1.digits_sum
Proof 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⟩
Proof 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
Theorem: Usa1992P1.digits_sum
Proof 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]
Proof 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
Theorem: Usa1992P1.digits_sum
Proof 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]
Proof 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
Theorem: Usa1992P1.digits_sum
Proof 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
Proof 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
Theorem: Usa1992P1.digits_sum
Proof 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
Proof 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