grind: normalization of `UInt16.toNat 0` gets in the way

[abentkamp]

Description

Goals around UInt16.toNat can sometimes fail because grind normalizes UInt16.toNat 0 too eagerly.

Context

Discussion here:
#general > grind confused by `UInt.toNat`?

Steps to Reproduce

example (b : UInt16) (h : b = 0) : UInt16.toNat b = 0 := by grind [UInt16.toNat_zero]

Expected behavior: grind should be able to prove this

Actual behavior: grind fails

Versions

4.28.0-nightly-2026-01-12 on live.lean-lang.org

Workaround

For the concrete example above, this is a possible workaround, but it feels like this should not be necessary:

@[grind gen]
theorem UInt16.toNat_of_eq_zero (h : b = 0) : UInt16.toNat b = 0 := by subst h; rfl