`suggest_for` 属性について調べる

こんな感じで使われている。

うっかり Unicode を使ったときに「君が欲しいのは Int じゃないかい？」ってサジェストする機能のために使われているっぽい。
（なぜ Lean リポの中で Unicode notation を用意しておかないのだろう…）

/--
The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
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.

  This constructor covers the non-negative integers (from `0` to `∞`).
  -/
  | ofNat   : Nat → Int
  /--
  The negation of the successor of a natural number is an integer.

  This constructor covers the negative integers (from `-1` to `-∞`).
  -/
  | negSucc : Nat → Int

Start with the shown Int declaration and its @[suggest_for ℤ] attribute. Trace where suggest_for is defined or handled in the Lean project, then document what the attribute does, why ℤ is associated with Int, and where the resulting suggestion appears.