chore: add HACK banner to isNonTrivialRegular transparency check

This PR adds a HACK comment to the transparency restriction in
`isNonTrivialRegular` so it's not forgotten. Per Sebastian's request
on Zulip.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/ExprDefEq.lean

@@ -1394,10 +1394,11 @@ private def isNonTrivialRegular (info : DefinitionVal) : MetaM Bool := do
     compares `instX a =?= instX b` with the correct transparency bump for
     instance-implicit parameters, which succeeds. -/
     if let some projInfo ← getProjectionFnInfo? info.name then
-      /- Only classify class projections as nontrivial at `.reducible` transparency,
+      /- HACK: Only classify class projections as nontrivial at `.reducible` transparency,
          since `unfoldDefault`'s extra `.instances` reduction (the reason for this classification)
          only applies there. At higher transparency levels, the normal unfolding behavior is
-         sufficient, and running the heuristic adds overhead without benefit. -/
+         sufficient, and running the heuristic adds overhead without benefit.
+         See https://github.com/leanprover/lean4/pull/12650 -/
       return projInfo.fromClass && backward.whnf.reducibleClassField.get (← getOptions) && (← getTransparency) == .reducible
     return false
   | .opaque => return false