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

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

State before:
n : ℕ
hn : 0 < n
⊢ (2 * 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
⊢ (2 * 10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10

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

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