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

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

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

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

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

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

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

State before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]
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_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]

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

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

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