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