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

State before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ all_one_or_two (Nat.digits 10 (prepend_two n))
Tactic:
rw [prepend_two_eq_append, all_one_or_two]
State after:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2

State before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2
Tactic:
rw [all_one_or_two] at hn
State after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2

State before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2
Tactic:
intro e he
State after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [2]
⊢ e = 1 ∨ e = 2

State before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [2]
⊢ e = 1 ∨ e = 2
Tactic:
rw [List.mem_append] at he
State after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ∨ e ∈ [2]
⊢ e = 1 ∨ e = 2

State before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ∨ e ∈ [2]
⊢ e = 1 ∨ e = 2
Tactic:
cases' he with he he
State after:
case inl
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n
⊢ e = 1 ∨ e = 2

case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [2]
⊢ e = 1 ∨ e = 2

State before:
case inl
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n
⊢ e = 1 ∨ e = 2
Tactic:
exact hn e he
State after:
no goals

State before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [2]
⊢ e = 1 ∨ e = 2
Tactic:
rw [List.mem_singleton] at he
State after:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 1 ∨ e = 2

State before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 1 ∨ e = 2
Tactic:
right
State after:
case inr.h
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 2

State before:
case inr.h
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 2
Tactic:
exact he
State after:
no goals