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

State before:
b k m n : ℕ
hm : 0 < m
hb : 1 < b
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
Tactic:
revert m
State after:
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)

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
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)

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
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)

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]
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)

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
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)

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
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)

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
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)

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
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)

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]
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)

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
State after:
no goals

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)]
State after:
no goals

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
State after:
no goals