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