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

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

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

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

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

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 = 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
⊢ (10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    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 + 10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length) / 10 =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10

State before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length) / 10 =
    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 + 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    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 + 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
exact add_comm _ _
State after:
no goals