WIP: bump to Lean 4.31.0-rc1

[dagurtomas]

Draft handoff PR for the Lean/mathlib v4.31.0-rc1 bump.

This preserves the partial progress from the bump session so others can continue from here. It is not ready to merge.

What is included:

• Earlier import/test import fixes from this branch.
• lean-toolchain bumped to leanprover/lean4:v4.31.0-rc1.
• mathlib pinned to v4.31.0-rc1.
• Compatibility updates across HoTTLean/ForMathlib, Grothendieck, groupoids, syntax, frontend, and typechecker files.
• A local Poly patch at patches/Poly-v4.31.0-rc1-local.patch, with short instructions in patches/README.md.
• Related Poly PR: Bump to Lean 4.31.0-rc1 Poly#37

Using the local Poly patch from a clean checkout:

lake update
git -C .lake/packages/Poly apply ../../../patches/Poly-v4.31.0-rc1-local.patch

Checks run at handoff:

• lake env lean HoTTLean/ForPoly.lean -DmaxErrors=10 passed, with existing sorry warnings and the expected local-Poly-changes warning.
• lake env lean HoTTLean/Groupoids/IsPullback.lean -DmaxErrors=5 failed; this is the current known blocker.

Known blockers / follow-up:

• HoTTLean/Groupoids/IsPullback.lean still fails, first at:
  ⊢ PreservesLimit (cospan (Cat.homOf tp') (Cat.homOf liftTy')) Core.map.
• The full lake build HoTTLean / lake build has not been repaired.
• The Poly dependency should eventually be updated to a real Poly branch/commit instead of relying on the local patch.
• Audit/remove WIP compatibility sorry placeholders before this is considered mergeable.