Error message from omega

Stream: new members

[Li Xuanji]

I don't understand the error message from omega here:

import Mathlib

example (n : ℕ) : (1 ≤ 2^n) := by
  omega

omega could not prove the goal:
a possible counterexample may satisfy the constraints
  a ≤ 0
where
 a := ↑2 ^ n

Is a an intermediate variable? Why is the 2 getting casted to ℤ? Is this just saying that an integer to a natural power could be negative?

(Actually this theorem could be proven with exact?, but I'm more used to trying omega first for goals involving only naturals, and the error message made me think that the theorem was false)

[Etienne Marion]

omega cannot handle goals where powers are variables. The error message does not really make sense here.

[Etienne Marion]

(I mean it comes from somewhere but we know 2^n cannot be nonpositive)

[Henrik Böving]

The error message does make sense, omega is trying to tell you that it understood 2 ^ n to be some opaque variable a because it doesn't understand what a power is and based on that assumption and the given constraints about a aka 2 ^ n it came to the conclusion that if a was <= 0 then the thing you want to prove wouldn't hold. And indeed if you think of 2 ^ n as just some a that is a valid concern to have.