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

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

State before:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.digits 10 n).length + n) % 10 = n % 10
Tactic:
rw [Nat.digits_len _ _ two_le_ten (ne_of_gt hn)]
State after:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10

State before:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10
Tactic:
rw [pow_add, pow_one]
State after:
n : ℕ
hn : 0 < n
⊢ (10 ^ Nat.log 10 n * 10 + n) % 10 = n % 10

State before:
n : ℕ
hn : 0 < n
⊢ (10 ^ Nat.log 10 n * 10 + n) % 10 = n % 10
Tactic:
exact Nat.mul_add_mod' _ 10 n
State after:
no goals