Theorem: ZerosOnesAndTwos.prepend_one_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_one n))
Tactic:
rw [prepend_one_eq_append, all_one_or_two]
State after:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], e = 1 ∨ e = 2

State before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], 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 ++ [1], e = 1 ∨ e = 2

State before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], 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 ++ [1]
⊢ e = 1 ∨ e = 2

State before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [1]
⊢ 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 ∈ [1]
⊢ 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 ∈ [1]
⊢ 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 ∈ [1]
⊢ 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 ∈ [1]
⊢ 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 = 1
⊢ e = 1 ∨ e = 2

State before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 1
⊢ e = 1 ∨ e = 2
Tactic:
simp only [he, OfNat.one_ne_ofNat, or_false]
State after:
no goals