feat: @[suggest_for ℤ] and @[suggest_for ℚ] annotations (#11596)

This PR adds `@[suggest_for ℤ]` on `Int` and `@[suggest_for ℚ]` on
`Rat`, following the pattern established by `@[suggest_for ℕ]` on `Nat`
in #11554.


🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <[email protected]>

Author: kim-em

src/Init/Data/Int/Basic.lean

@@ -42,6 +42,7 @@ larger numbers use a fast arbitrary-precision arithmetic library (usually
 than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
 architectures).
 -/
+@[suggest_for ℤ]
 inductive Int : Type where
   /--
   A natural number is an integer.

src/Init/Data/Rat/Basic.lean

@@ -20,6 +20,7 @@ Rational numbers, implemented as a pair of integers `num / den` such that the
 denominator is positive and the numerator and denominator are coprime.
 -/
 -- `Rat` is not tagged with the `ext` attribute, since this is more often than not undesirable
+@[suggest_for ℚ]
 structure Rat where
   /-- Constructs a rational number from components.
   We rename the constructor to `mk'` to avoid a clash with the smart constructor. -/