Persuading Even's to be less general

Stream: lean4

[Siddhartha Gadgil]

Even's becoming very general recently has meant the code below has a typeclass inference issue in spite of my attempts to give a high priority typeclass. Does anyone have any suggestions, other than the obvious one I have included.

For context, instance is better as this is meant to be used in AI generated code, and adding context is cleaner than rewriting.

import Mathlib

instance (priority := high) : Add ℤ := inferInstance

example : {n | Even n}.Infinite := by sorry /- typeclass instance problem is stuck, it is often due to metavariables
  Add ?m.606
-/

example : {n : ℤ  | Even n}.Infinite := by sorry -- works but want to avoid

[Kyle Miller]

Making it be a high-priority instance works to make it apply over other instances, but it's not enough to make Lean commit to using the instance even though it involves specializing a metavariable.

Default instances are a way to get Lean to commit to an instance if nothing else applies.

@[default_instance]
instance : Add ℤ := inferInstance

[Siddhartha Gadgil]

Thanks. That's perfect.