Theorem: ZerosOnesAndTwos.prepend_two_eq_append (Compfiles/ZeroesOnesAndTwos.lean)

State before:
n : ℕ
⊢ Nat.digits 10 (prepend_two n) = Nat.digits 10 n ++ [2]
Tactic:
induction' n using Nat.strong_induction_on with n' ih
State after:
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two n') = Nat.digits 10 n' ++ [2]

State before:
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two n') = Nat.digits 10 n' ++ [2]
Tactic:
cases' n' with n'
State after:
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two 0) = Nat.digits 10 0 ++ [2]

case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two (n' + 1)) = Nat.digits 10 (n' + 1) ++ [2]

State before:
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two 0) = Nat.digits 10 0 ++ [2]
Tactic:
norm_num [prepend_two]
State after:
no goals

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two (n' + 1)) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [Nat.digits_def' two_le_ten (prepend_two_pos _)]
State after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [2]

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [prepend_two_div _ (Nat.succ_pos n')]
State after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
have hns : n'.succ / 10 < n'.succ := Nat.div_lt_self' n' 8
State after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [ih _ hns]
State after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [2]) = Nat.digits 10 (n' + 1) ++ [2]

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [2]) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [←List.cons_append]
State after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [2] = Nat.digits 10 (n' + 1) ++ [2]

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [2] = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [prepend_two_mod _ (Nat.succ_pos _), ←Nat.digits_def' two_le_ten (Nat.succ_pos n')]
State after:
no goals