omega does not look through abbreviations in types

[nomeata]

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.