rw [List.mem_singleton] at he
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [1]
⊢ 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