Sync upstream mathlib4 (2026-07-27, +5 commits) - #86
Merged
Merged
Conversation
…42084) Apparently giving the proof explicitly allows us to remove the backward.inferInstanceAs.wrap`. Note that avoiding the defeq abuse by first doing `dsimp` still does not work (and interesting replacing the `:=` with `:= by exact` does not work as well). This removes the [last]([#mathlib4 > Technical Debt Counters @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Technical.20Debt.20Counters/near/611588552)) `backward.inferInstanceAs.wrap` exception from the technical debt counter. The solution was found with GPT 5.6 Sol high (fairly quickly) Co-authored-by: Batixx <s59fpern@uni-bonn.de>
A test file is added to ensure that certain "dsimplifying" equalites in category theory are tagged with `@[defeq]` instead of `@[backward_defeq]`, so that `dsimp` can use them without `set_option backward.defeqAttrib.useBackward true`. To turn a `@[backward_defeq]` into a `@[defeq]`, definitions need to be made `implicit_reducible`. Now that `instance_reducible` is split off `implicit_reducible`, it is much safer to tag many declarations. There is still a ton of declarations that should be tagged, and I did not remove all `set_options` after this tagging (this should be an automated process), but we can already clear some.
…ing"]` syntax (#41886) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…egree of `0` (#34759)
`withBotDegree` is to distinguish the degree of zero polynomial from the degree of non-zero constant polynomial. `MonomialOrder.degree` of both are 0, while `withBotDegree` is `⊥` for zero polynomial and 0 for non-zero constant polynomial.
Some lemmas, such as $\mathrm{degree} (p * q) = \mathrm{degree}(p) + \mathrm{degree}(q)$, hold on edge cases where $p=0$ or $q=0$ under `MonomialOrder.withBotDegree` but not `MonomialOrder.degree`.
`MonomialOrder.withBotDegree` is to `MonomialOrder.degree` as `Polynomial.degree` is to `Polynomial.natDegree`.
It's upstreamized from https://github.com/WuProver/groebner_proj.
…isms (#42065) Correct docstring about preservation of epimorphisms.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Automated daily sync from
leanprover-community/mathlib4@master.65fe2a1f85b506b0ef7df1990697be5a1ad64317Auto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Low Risk
Mostly attribute, documentation, and new API alongside tests; no auth or runtime infrastructure changes. The monomial
withBotDegreeblock is large but additive library surface.Overview
Upstream mathlib4 sync (5 commits) adapting to Lean 4.31 definitional-equality behavior: many category-theory
defs and key equivalences now carry@[implicit_reducible]so@[simps]lemmas stay on@[defeq]fordsimp, with relatedbackward.*set_options removed where no longer needed. AddsMathlibTest/CategoryTheory/CheckDsimp.leanto guard important simp/defeq tags.Monomial orders:
MonomialOrder.toWithBotSynand scoped≼'[m]/≺'[m]onWithBot (σ →₀ ℕ);MonomialOrder.withBotDegreeonMvPolynomial(degree⊥for zero, parallel tonatDegreevsdegree).Smaller fixes:
CommShift₂precomposition usesCommShift.compinstead ofinferInstanceAs; Yoneda/shrinkYoneda/coyoneda lemma tweaks (dsimp%, proof fixes);to_additivedocstrings viadocCommentonly (drops deprecatedstrsyntax); doc typo on projective preservation vs epimorphisms.Reviewed by Cursor Bugbot for commit c51e170. Bugbot is set up for automated code reviews on this repo. Configure here.