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

State before:
n : ℕ
hn : 0 < n
⊢ prepend_two n / 10 = prepend_two (n / 10)
Tactic:
rw [prepend_two, prepend_two]
State after:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) / 10 = 2 * 10 ^ (Nat.digits 10 (n / 10)).length + n / 10

State before:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) / 10 = 2 * 10 ^ (Nat.digits 10 (n / 10)).length + n / 10
Tactic:
cases' n with n
State after:
case zero
hn : 0 < 0
⊢ (2 * 10 ^ (Nat.digits 10 0).length + 0) / 10 = 2 * 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10

case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case zero
hn : 0 < 0
⊢ (2 * 10 ^ (Nat.digits 10 0).length + 0) / 10 = 2 * 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10
Tactic:
cases Nat.lt_asymm hn hn
State after:
no goals

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [digits_len' n.succ (Nat.succ_pos n)]
State after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [pow_add, pow_one, add_comm]
State after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 2 * (10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 2 * (10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [←mul_left_comm]
State after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * (2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * (2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [Nat.add_mul_div_left _ _ (Nat.succ_pos 9)]
State after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1) / Nat.succ 9 + 2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1) / Nat.succ 9 + 2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
exact add_comm _ _
State after:
no goals