[CONFLICT] Sync upstream mathlib4 (2026-05-12)

[winstonyin-ax]

Automated daily sync from leanprover-community/mathlib4@master.

• Upstream tip: 1b6d4054371387401ef58e4593a47b0317e8862b
• Commits being merged: 5
• Run: https://github.com/Axiomatic-AI/mathlib4/actions/runs/25718807051

⚠️ Merge conflicts

The merge commit on this branch contains conflict markers, so CI will fail
and auto-merge will not run. Resolve manually:

git fetch origin && git checkout sync/upstream
# edit conflicted files to remove markers, then:
git commit --amend --no-edit
git push --force-with-lease

Files with conflict markers

---

Note

High Risk
High risk because .github/actions/get-mathlib-ci/action.yml still contains unresolved conflict markers that will break CI, and the changes touch core tactic/attribute generation (reassoc, translation insertion) which can cause widespread downstream breakage.

Overview
Syncs upstream mathlib4 by moving Northcott into Mathlib.Order.Northcott and updating imports accordingly (including the Mathlib.lean umbrella import list).

Adds/normalizes a handful of inner product space simp lemmas (e.g. adjoint_id, adjoint_one, id_mem_unitary, IsSymmetric.one) and adjusts permutation sign results (sign_finRotate) with corresponding simplification in Alternating.lean.

Refactors category-theory attribute infrastructure: consolidates reassoc into a generating attribute implementation and updates translation insertion to avoid duplicating existing translations, alongside minor to_additive/reassoc attribute annotation cleanups.

Notably, the PR currently introduces an unresolved merge conflict in .github/actions/get-mathlib-ci/action.yml (conflict markers in the pinned ref), and updates upstream_sha.

^{Reviewed by Cursor Bugbot for commit 0e5f506. Bugbot is set up for automated code reviews on this repo. Configure here.}