Sync upstream mathlib4 (2026-07-25, +34 commits) - #84
Merged
Merged
Conversation
All these definitions are noncomputable (because they use choice/produce sets), but the computability checker doesn't spot this until I try making `Set` a one-field structure. This is because the computability checker doesn't even try to compute sorts, but it doesn't see that `s : Set α` is (equivalent to) a family of sorts.
I need this in a later PR. Also take the opportunity to use `deriving` for two out of the three instances.
…tolabel` (#34952) - use `Cli` for `lake exe autolabel` - add arguments `--pr xxx --gh` and `--pr xxx --curl <TOKEN>` to chose between different interaction methods with github - add `--force` to skip the check whether labels are already present. (note: the current `curl` setup doesn't perform this step and neither does the refactor, so I added a `Todo` to remember this. ) - make CI-workflow simpler and more robust by removing current stdout-parsing of the debug-messages which `autolabel` emits. - remove CI-trigger on `push`: this was useful back in the days when PRs happened on mathlib4-branches, as it allowed changes to the workflow to be tested directly in the PR. Since this used a security gap which has been closed since, we remove that code completely. ### Testing Make some local changes and commit them. Ensure your local `origin/master` is in sync with `upstream/master` if you are on a fork. - `lake exe autolabel`: prints the labels which would be applicable - `lake exe autolabel --pr 34952 --gh --force` adds these labels to this PR using `gh`. - `lake exe autolabel --pr 34952 --gh` adds these labels to this PR using `gh` if no topic labels are present. - `lake exe autolabel --pr 34952 --curl <ACCESS_TOKEN>` adds these labels to this PR using `curl`. This requires a github access token for authentication
Co-authored-by: Batixx <s59fpern@uni-bonn.de>
Per naming convention, defs should not have underscores in their name. This is also counted as strong technical debt, according to the counter we have 493 right now. This PR fixes all of them in Mathlib/Order except one, namely [RelIso.Simps.symm_apply](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/RelIso/Basic.html#RelIso.Simps.symm_apply), which is a bit weird. All renames here are quite simple, just go from `snake_case` to `lowerCamelCase` (+ add deprecations). If this PR looks good, i would be happy to do this to the (vast majority of) other defs with underscore in mathlib. :) Co-authored-by: Batixx <s59fpern@uni-bonn.de>
Replace a big `simp` with `rfl`, which speeds up kernel typechecking and removes a `set_option backward.isDefEq.respectTransparency false`. Remove two `have` lines in `instance (i : ι) : Algebra.IsSeparable (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯)` which speeds up kernel typechecking. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/kernelbarfing.20in.20mathlib/near/609873490).
…874) This PR golfs some proofs, removes local notation (which means the theorem displays more nicely in Loogle + docs), and removes some `set_option backward.isDefEq.respectTransparency.types false in`. [](https://gitpod.io/from-referrer/)
This is enabled by default to make eg i^5 simplify automatically. We intentionally require the exponent to be a numeral, as this is intended to be a reduction statement, and for symbolic `n`, the lemma `I_pow_eq_pow_mod` should be used instead. Note that we can't have `I_pow_eq_pow_mod` as a simp lemma due to looping.
…rmDet (#42058) move the determinant normalization simproc `norm_det` and `eval_det` tactic to `Tactic/NormDet` in preparation for generalizing the tactic to work with mathlib Matrix determinants: #42059.
The documentation of `StrictUniversalPropertyFixedTarget` was slightly misleading. This PR updates it to better reflect the fields of the structure.
…2061) The new name is better anyway, and simplifies life for the `blanketSimpArgs` linter in #42056: cherry-picked from that PR. Co-authored-by: sgraf812 <1151264+sgraf812@users.noreply.github.com>
… (#42059) Previously the `norm_det` simproc / `eval_det` tactic normalized Bird determinants, i.e `BirdDet.birdDet`. This commit changes `norm_det` to normalize `Matrix.det` calls, using #41160 to connect Bird's determinant with `Matrix.det`. Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
…tended type (#42053) `Subsingleton.eq_zero` and `Subsingleton.eq_one` have a bare variable as their LHS, so as simp lemmas they are tried on every visited subterm, and each attempt runs a `Subsingleton` instance search. Pinning the type argument at the call site makes unification fail cheaply on all other subterms and confines the instance search to the type actually being collapsed. Instruction counts for `lake env lean` on v4.33.0-rc1: `Mathlib.Algebra.Central.End` drops from 14.8G to 8.2G. The remaining call sites show the same pattern at smaller scale.
…062) This PR was automatically created from PR #42056 by @sgraf812 via a [review comment](leanprover-community/mathlib4#42056 (comment)) by @grunweg. Co-authored-by: sgraf812 <1151264+sgraf812@users.noreply.github.com>
…valued indicator (#40909) Adds `Set.mulIndicator_apply_apply` and its `to_additive` companion `Set.indicator_apply_apply`: for a family of functions `f : α → β → M`, `s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a`, so evaluating a function-valued indicator at `b` commutes with the indicator. It is the pointwise form of `Set.mulIndicator_comp_of_one` (with `g` the evaluation map at `b`).
…r_series` in comment (#41954) This PR fixes an occurrences of `mv_power_series` from the Lean 3 days. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
This PR sets `pp.mvars.anonymous false` for `MathlibTest` in the lakefile, and removes the now-superfluous `set_option`s which did so in individual tests. In tests, we always want to set this option (which pretty-prints autogenerated mvars such as `?m.37` as `?_`) to ensure that they are stable. Instead of looking for it during review, we can just have it always set to the correct value by default. In fact, this PR also catches some unstable tests which slipped past during review. It also documents the decision to not use the standard mathlib options, and removes stale documentation around `mathlibLeanOptions`. (Note: `mathlibLeanOptions` implicitly says that tests should use ``⟨`maxSynthPendingDepth, .ofNat 3⟩``, but we've been getting by just fine without that.) So far this is the only option for `MathlibTest`, but we may as well still put it in an array to hold the documentation and not interrupt the flow of `lean_lib`s. (And maybe make it easier set other options for MathlibTest in the future if we find we need them.)
…ated names (#41653) These were incorrectly deprecated as part of a rename in #39494 because the namespace `MonomialOrder` was missing. We fix this here.
…g API for `LocallyIntegrableOn` (#41733) Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
This one proof was taking a huge amount of time to typecheck, presumably because of some defeq abuse. Fixing this up gives a nice speedup in this file.
Given a Nodup list: * If a prefix contains the last element, they are equal * If a suffix contains the first element, they are equal * If an infix contains the first element, it is a prefix * If an infix contains the last element, it is a suffix * If the first and the last element are the same, it is a singleton * `countP` is cardinality of the filter of `toFinset`. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Oliver Nash <github@olivernash.org>
…… (#42031) …clideanQuadrant implicit_reducible This allows removing some technical debt and fixes all but two warnings of the linter.tacticCheckInstances linter in this file. (The remaining ones are about identifying membership in Set.Icc with the conjuction of the two individual hypotheses, i.e. are unrelated to this file.)
… zero or one (#41987)
… (#41138) A simple lemma about iterating the derivative
Fix the argument names of `FreeMonoid.recOn`, `FreeMonoid.inductionOn`, and `FreeMonoid.inductionOn'`. Name the motive `motive` and name the minor premises according to their contents.
…213) `GroupTheory/Torsion.lean` has some bad to_additive translations. This PR fixes this by renaming `Monoid.IsTorsion` to `IsMulTorsion` and `AddMonoid.IsTorsion` to `IsAddTorsion`. This also aligns better with `IsMulTorsionFree` and `IsAddTorsionFree`. This PR has a lot of deprecations, but you can check the lean-aware declarations diff to make sure I didn't miss anything. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
Similar (motivation) to #42063. This PR removes all newlines between public imports. This is not important as standalone PR, but makes diffs of later PRs nicer and thus help reviewing. This includes space between ordinary public and `public meta` imports (and imports from Lean core). Maybe there should be a convention on there to be a newline for those cases, but this is not currently done in the vast majority of cases and not the scope of this PR. Also some import orders of affected files are not ordered alphabetically still, which I did not fix as this is again not the goal of this PR. Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…39558) Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…#41566) This PR fixes the malformed deprecation date `since := "26/06/2026"` on the `res_map_hom_toLinearMap` alias in `Mathlib/RepresentationTheory/Rep/Res.lean`, changing it to the standard `YYYY-MM-DD` form `"2026-06-26"`. It was the only deprecation date in Mathlib not in this format, which breaks date-based deprecation tooling. Follow-up to [#41054 (refactor(RepresentationTheory/Rep/Res): refactor resFunctor)](leanprover-community/mathlib4#41054). 🤖 Prepared with Claude Code
Discovered while auditing the uses of that lemmas, for reviewing #42053.
…restricted multivariate power series (#39583) Previously, restricted power series were defined in terms of a `tendsto atTop` this has been changed to be an abbrev of `MvPowerSeries.IsRestricted` with `isRestricted_iff` lemmas to convert to nicer usable definitions. Co-authored-by: WilliamCoram <williamecoram@gmail.com>
](https://gitpod.io/from-referrer/){kind=link}
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
20 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.3bc2a1801c2416549ba5ba0b3f5728a28b87e7d9Auto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Medium Risk
Large automated sync touching core algebra (torsion, NNRat), tactics, and measure theory; renames are deprecated but widespread, so downstream code depending on old names or computable
Setdefs may need updates.Overview
This merges 34 upstream commits into the vendored Mathlib tree, mainly API maintenance and proof hygiene rather than new mathematical content.
Naming and deprecations: Multiplicative/additive torsion predicates move to top-level
IsMulTorsion/IsAddTorsion(with@[deprecated]aliases for oldMonoid.IsTorsionnames).Data.NNRat.Orderis deprecated in favor of newAlgebra.Order.Ring.NNRat; imports across combinatorics, measure theory, and rat-related files follow. Several Boolean/Galois/Filter helpers get camelCase names (e.g.distribLatticeOfSSupEqTop,giSSupIic,giPrincipalKer,Fin.homSucc).New pieces:
Mathlib.Tactic.NormDet(and related determinant Bird imports reshuffled inMathlib.lean),Algebra.Order.Ring.NNRat, aComplex.Ipowersimproc, and small lemmas (e.g.Matrix.ofArray_ofFn, off-diagonal pair counts, listNodupinfix lemmas,LocallyIntegrablecontinuous mul/smull helpers).Computability / defs: Many definitions returning
Setare markednoncomputablewith notes pointing at Lean #14084 (graph partitions, measure-theory helpers, group-theory transfer, etc.).finrankSupport,centeredArc, and similar defs get the same treatment.Proof and linter churn:
FreeMonoidrecursors/induction use renamed motive branches (of_mulvsmul_of) andrecOn-based proofs;zpow_zero/zpow_onelose directsimptags (simpNF) while additive counterparts staysimp; proofs swapfield_simp/ flexible linter blocks forgrind,rfl, or explicitSubsingleton.eq_zero (α := …);Algebra.Order.Antidiag.Pidrops transparency hacks and simplifies disjointness proofs.Risk: Broad touch surface across algebra, measure theory, and tactics, but changes are largely mechanical renames,
noncomputableannotations, and proof simplifications aligned with upstream Mathlib.Reviewed by Cursor Bugbot for commit 5532a08. Bugbot is set up for automated code reviews on this repo. Configure here.