omega does not look through abbreviations in types

I would expect this to work

example (x : Fin 3) : x ≠ x + 1 := by omega

abbrev Foo := Fin 3

/--
error: omega could not prove the goal:
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
-/
#guard_msgs in
example (x : Foo) : x ≠ x + 1 := by omega

without this, I get penalized for introducing nice names for some of my abstractions. Most other parts of the system can look through abbreviations (e.g. name resolution, type class inference), so omega should maybe too.

Probably just a matter of calling whnfR in the right place.

Versions

"4.12.0-nightly-2024-10-15"

Additional Information

Wanted to use this in https://github.com/teorth/equational_theories/pull/599.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the omega tactic and run the reproducer in the issue, comparing the direct Fin 3 example with the Foo abbreviation example. Investigate the mentioned whnfR path for type handling. Done means omega proves the abbreviated-type goal while preserving the existing direct example behavior.