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

[winstonyin-ax]

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

• Upstream tip: e9da88d74d4f24032858100ad765d947c57e94a0
• Commits being merged: 40
• Run: https://github.com/Axiomatic-AI/mathlib4/actions/runs/25846748384

⚠️ 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 due to changes in core simp/meta tooling (Simp.withoutTheorems, eqComm simproc, new simp attrs) and broad foundational refactors, plus an unresolved conflict marker in .github/actions/get-mathlib-ci/action.yml that will break CI until fixed.

Overview
Pulls in an upstream snapshot with broad library updates, including new modules Analysis/Complex/BranchLogRoot, RingTheory/LocalRing/MaximalIdeal/Square, and a deprecated shim Geometry/Manifold/VectorBundle/SmoothSection, plus corresponding Mathlib.lean import updates.

Refactors algebraic foundations: lowers instance priority for EuclideanDomain.toCommRing, generalizes Submodule/LinearMap.restrict to →ₛₗ, replaces several CanonicallyOrderedAdd requirements with IsBotZeroClass and adds IsBotZeroClass/OrderBot instances for Finsupp/DFinsupp (and Lex/Colex), and introduces an Ideal.IsMinimalPrime API with widespread updates from h.1.1-style projections to h.isPrime/h.le.

Adds new simp/meta infrastructure: Lean/Meta/Simp.lean gains Simp.withoutTheorems, Logic/Basic.lean adds eqComm/iffComm simprocs, and Tactic/Attr/Register.lean registers pull_end/push_end simpsets; many lemmas are updated to use these (eqComm, pull_end) and some old simp lemmas are deprecated.

CI/automation changes include a new scheduled/manual shake GitHub workflow that runs lake shake --fix and opens a PR + posts to Zulip, and the get-mathlib-ci composite action currently contains unresolved merge conflict markers that must be resolved for CI to pass.

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

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 8fb9087. Configure here.}

[cursor]

Unresolved nested merge conflict markers in YAML action

High Severity

The file contains nested git merge conflict markers (<<<<<<< HEAD, =======, >>>>>>> upstream/master), making it invalid YAML. This breaks the get-mathlib-ci composite action — any workflow referencing this action will fail to parse the default value for the ref input. The outer conflict markers are newly introduced by this commit on top of pre-existing inner conflict markers, resulting in a doubly-conflicted file that needs manual resolution.

 

^{Reviewed by Cursor Bugbot for commit 8fb9087. Configure here.}