From baa71faf87812449640c64bfd7b1eaf553669044 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 24 Mar 2026 06:31:56 +0000 Subject: [PATCH 01/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13086 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 73680c6061faeb..7f92087e269a9a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "81c23850e7c2b5f82ed16e3569def2fe0f52e1c9", + "rev": "1eec0f14788781254d00b4ebb9628d3d1e322aa0", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-13086", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 1de37822c9c419..fd3bb7a2e3f178 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-13086" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.92-pre1" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index de7cb2ba9bc582..93d8de5b14c947 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-03-24 +leanprover/lean4-pr-releases:pr-release-13086-4bf0162 From cbf62a73eed9c13f1266afbf60dbf0ae53a4316f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 24 Mar 2026 06:47:26 +0000 Subject: [PATCH 02/77] feat: add `Lean.Grind.PowIdentity` instance for finite fields This provides a `PowIdentity K (Fintype.card K)` instance for any finite field, based on `FiniteField.pow_card` (Fermat's little theorem). This allows the `grind` ring solver to reduce high-degree polynomials over finite fields. Co-Authored-By: Claude Opus 4.6 (1M context) --- Mathlib/FieldTheory/Finite/Basic.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean index e55699cdd5960a..840047198a8c1e 100644 --- a/Mathlib/FieldTheory/Finite/Basic.lean +++ b/Mathlib/FieldTheory/Finite/Basic.lean @@ -239,6 +239,16 @@ theorem pow_card_pow (n : ℕ) (a : K) : a ^ q ^ n = a := by end +section + +variable [Field K] [Fintype K] + +open Lean in +instance instGrindPowIdentity : Grind.PowIdentity K (Fintype.card K) where + pow_eq := pow_card + +end + variable (K) [Field K] [Fintype K] /-- The cardinality `q` is a power of the characteristic of `K`. -/ From f420f53631e699aad89e365929c6d0c6e325f331 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 26 Mar 2026 11:10:53 +0000 Subject: [PATCH 03/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13132 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 73680c6061faeb..939fcc3af15339 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "81c23850e7c2b5f82ed16e3569def2fe0f52e1c9", + "rev": "147d8a6d5692649259bfa3f8c5ea6a9385aeac88", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-13132", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 1de37822c9c419..a52a5fdfd39591 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-13132" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.92-pre1" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index de7cb2ba9bc582..bb75ca220ada74 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-03-24 +leanprover/lean4-pr-releases:pr-release-13132-5594b54 From 28dc0ab2d625951424b570d7c7430d32d9e142ae Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 26 Mar 2026 13:34:51 +0000 Subject: [PATCH 04/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13132 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 939fcc3af15339..233d9ebd62a56d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "147d8a6d5692649259bfa3f8c5ea6a9385aeac88", + "rev": "943cd21dabe73116cc96d7ec7e0242deaa6dc0cd", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13132", diff --git a/lean-toolchain b/lean-toolchain index bb75ca220ada74..9020076871b042 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13132-5594b54 +leanprover/lean4-pr-releases:pr-release-13132-2f8db4b From d7aee7edce0743c7500b1de8cc72a05564d8c37e Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 26 Mar 2026 14:18:43 +0000 Subject: [PATCH 05/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13132 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 233d9ebd62a56d..d47be9b382b89e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "943cd21dabe73116cc96d7ec7e0242deaa6dc0cd", + "rev": "257610310763a697d819165a58f209a63a512929", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13132", diff --git a/lean-toolchain b/lean-toolchain index 9020076871b042..363e30b7f1ae7f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13132-2f8db4b +leanprover/lean4-pr-releases:pr-release-13132-8479ef4 From deb87e3dd5774ef3467b8cbd52cf88dabf6f16bb Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Apr 2026 00:28:04 +0000 Subject: [PATCH 06/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13223 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e435c475740f43..c668987c11650a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "81df60304bb26e3e1efc6ee9b07fb387dac19108", + "rev": "3d5a3aaab3de9235f10521681974f5043f072f09", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-13223", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 8fa4ac638fc9fb..da7aa856d361a7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-13223" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "nightly-testing" diff --git a/lean-toolchain b/lean-toolchain index 3911411c451a70..30316b1566a727 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-03-31 +leanprover/lean4-pr-releases:pr-release-13223-f92b7f3 From b465a60109aafff3a6fb36128332d23780a9ef49 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Apr 2026 11:06:57 +0000 Subject: [PATCH 07/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13229 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c6f5dc8152dce1..bd012465e8def1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "da8a068708756fcc8aa953efc0dd95094b73a934", + "rev": "c0286d9a17937d9e498f0bb3c499d97eceb05ba9", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-13229", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 1de37822c9c419..ba4571d0983075 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-13229" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.92-pre1" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index b222dcbd6a2d8b..5f005db8ca8aa7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-03-25 +leanprover/lean4-pr-releases:pr-release-13229-f76c89f From f841c8f402a15bf6f36f482cb7aa95dcdc7ae90a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 31 Mar 2026 20:30:03 +0000 Subject: [PATCH 08/77] chore: indent tactic blocks after `by` and `decreasing_by` Adapt to leanprover/lean4#13217 which requires indented tactic sequences after `by` and `decreasing_by`. Co-Authored-By: Claude Opus 4.6 --- Mathlib/RingTheory/MvPolynomial/Groebner.lean | 14 +++++++------- .../RingTheory/Valuation/ValuativeRel/Basic.lean | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Mathlib/RingTheory/MvPolynomial/Groebner.lean b/Mathlib/RingTheory/MvPolynomial/Groebner.lean index c6abb237cd5a93..2be50c65a7fcde 100644 --- a/Mathlib/RingTheory/MvPolynomial/Groebner.lean +++ b/Mathlib/RingTheory/MvPolynomial/Groebner.lean @@ -213,13 +213,13 @@ theorem div {ι : Type*} {b : ι → MvPolynomial σ R} termination_by WellFounded.wrap ((isWellFounded_iff m.syn fun x x_1 ↦ x < x_1).mp m.wf) (m.toSyn (m.degree f)) decreasing_by -· exact deg_reduce -· apply degree_sub_LTerm_lt - intro hf0 - apply hf'0 - simp only [subLTerm, sub_eq_zero] - nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0] - simp + · exact deg_reduce + · apply degree_sub_LTerm_lt + intro hf0 + apply hf'0 + simp only [subLTerm, sub_eq_zero] + nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0] + simp /-! Module doc as workaround for a parser error that prevents using `set_option` diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean index 162e0f42544bc5..5c424ace955138 100644 --- a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean +++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean @@ -1214,10 +1214,10 @@ theorem orderMonoidIso_embed [v.Compatible] {Γ' : Type*} [LinearOrderedCommGrou (w : Valuation R Γ') [w.Compatible] (x : ValueGroupWithZero R) (h : w.IsEquiv v) : h.orderMonoidIso (embed w x) = embed v x := by -simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk] -induction x using ValueGroupWithZero.ind with -| mk r s => - simp + simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk] + induction x using ValueGroupWithZero.ind with + | mk r s => + simp /-- If a valuation `v` is compatible with the valuative relation, then `ValueGroupWithZero R` is isomorphic to the image group (with zero) of `v` as an ordered group with zero. -/ From b779d444a383d24980a644ea05c9cc14cf220ab3 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 31 Mar 2026 21:42:55 +0000 Subject: [PATCH 09/77] chore: indent tactic block in EmptyLine test Adapt to leanprover/lean4#13217. Co-Authored-By: Claude Opus 4.6 --- MathlibTest/EmptyLine.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/MathlibTest/EmptyLine.lean b/MathlibTest/EmptyLine.lean index 41a11e48d8e824..637a9d5ad5b0e5 100644 --- a/MathlibTest/EmptyLine.lean +++ b/MathlibTest/EmptyLine.lean @@ -159,31 +159,31 @@ example : True := by -- The following empty line is not reported, since the com warning: Please, write a comment here or remove this line, but do not place empty lines within commands! Context: ↓ - ⏎example : True := by⏎⏎-- Here I start⏎⏎ + ⏎example : True := by⏎⏎ -- Here I start⏎⏎ Note: This linter can be disabled with `set_option linter.style.emptyLine false` --- warning: Please, write a comment here or remove this line, but do not place empty lines within commands! Context: - ↓ - ⏎--stop⏎⏎trivial⏎⏎ + ↓ + ⏎ --stop⏎⏎ trivial⏎⏎ Note: This linter can be disabled with `set_option linter.style.emptyLine false` -/ #guard_msgs in example : True := by --- Here I start + -- Here I start -/- + /- --/ + -/ ---stop + --stop -trivial -- also a comment + trivial -- also a comment --- with a line break + -- with a line break -- Check that `where` fields allow empty lines. structure F where From 61a6a0f78945b722e3142fc7e20959c2e6af76d1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 1 Apr 2026 12:32:02 +0000 Subject: [PATCH 10/77] chore: indent expression continuations at column 0 Co-Authored-By: Claude Opus 4.6 --- Mathlib/Algebra/Module/Submodule/LinearMap.lean | 2 +- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean | 2 +- Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Module/Submodule/LinearMap.lean b/Mathlib/Algebra/Module/Submodule/LinearMap.lean index 68d86fc001983e..5654a2b9333ef0 100644 --- a/Mathlib/Algebra/Module/Submodule/LinearMap.lean +++ b/Mathlib/Algebra/Module/Submodule/LinearMap.lean @@ -177,7 +177,7 @@ theorem subtype_comp_codRestrict (p : Submodule R₂ M₂) (h : ∀ b, f b ∈ p section variable {M₂' : Type*} [AddCommMonoid M₂'] [Module R₂ M₂'] -(p : M₂' →ₗ[R₂] M₂) (hp : Injective p) (h : ∀ c, f c ∈ range p) + (p : M₂' →ₗ[R₂] M₂) (hp : Injective p) (h : ∀ c, f c ∈ range p) /-- A linear map `f : M → M₂` whose values lie in the image of an injective linear map `p : M₂' → M₂` admits a unique lift to a linear map `M → M₂'`. -/ diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index dd08bd9caf1a31..495ccb223bb43c 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -269,7 +269,7 @@ end CompleteSpace section Pi variable {ι : Type*} {X : α → Type*} [∀ x, CommMonoid (X x)] [∀ x, TopologicalSpace (X x)] -{L : SummationFilter ι} + {L : SummationFilter ι} @[to_additive] theorem Pi.hasProd {f : ι → ∀ x, X x} {g : ∀ x, X x} : diff --git a/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean b/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean index 226f4e4d1ab33f..dbc911b2b241b8 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean @@ -17,7 +17,7 @@ public section open UniformSpace.Completion variable {α β : Type*} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] -{L : SummationFilter β} + {L : SummationFilter β} /-- A function `f` has a sum in a uniform additive group `α` if and only if it has that sum in the completion of `α`. -/ From e714425c284fd251369c2199cbc57a83f9f0b9ac Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 1 Apr 2026 13:14:06 +0000 Subject: [PATCH 11/77] chore: indent expression continuations at column 0 Co-Authored-By: Claude Opus 4.6 --- Mathlib/Analysis/Analytic/ChangeOrigin.lean | 2 +- Mathlib/Analysis/Normed/Module/Ray.lean | 2 +- Mathlib/Analysis/Normed/Operator/Basic.lean | 2 +- .../Geometry/Manifold/Algebra/LieGroup.lean | 2 +- Mathlib/MeasureTheory/Measure/AddContent.lean | 2 +- .../VectorMeasure/AddContent.lean | 2 +- Mathlib/RingTheory/Ideal/Maps.lean | 24 +++++++++---------- 7 files changed, 18 insertions(+), 18 deletions(-) diff --git a/Mathlib/Analysis/Analytic/ChangeOrigin.lean b/Mathlib/Analysis/Analytic/ChangeOrigin.lean index 19d6228da2c365..b95041cfe9ed39 100644 --- a/Mathlib/Analysis/Analytic/ChangeOrigin.lean +++ b/Mathlib/Analysis/Analytic/ChangeOrigin.lean @@ -43,7 +43,7 @@ open scoped NNReal ENNReal Topology open Filter Set variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] -[NormedAddCommGroup F] [NormedSpace 𝕜 F] + [NormedAddCommGroup F] [NormedSpace 𝕜 F] namespace FormalMultilinearSeries diff --git a/Mathlib/Analysis/Normed/Module/Ray.lean b/Mathlib/Analysis/Normed/Module/Ray.lean index ceb5c4bad4b473..e64bc5f6d23f02 100644 --- a/Mathlib/Analysis/Normed/Module/Ray.lean +++ b/Mathlib/Analysis/Normed/Module/Ray.lean @@ -22,7 +22,7 @@ public section open Real variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} -[NormedAddCommGroup F] [NormedSpace ℝ F] + [NormedAddCommGroup F] [NormedSpace ℝ F] namespace SameRay diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean index 45fe5b39d6fd4d..d248d0f8e9c2df 100644 --- a/Mathlib/Analysis/Normed/Operator/Basic.lean +++ b/Mathlib/Analysis/Normed/Operator/Basic.lean @@ -79,7 +79,7 @@ theorem closedBall_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : by simp_all⟩ variable {F' 𝓕' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [Nontrivial F'] -{τ : 𝕜 →+* ℝ} [FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F'] + {τ : 𝕜 →+* ℝ} [FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F'] theorem sphere_subset_range_iff_surjective [RingHomSurjective τ] {f : 𝓕'} {x : F'} {r : ℝ} (hr : 0 < r) : sphere x r ⊆ Set.range f ↔ (⇑f).Surjective := by diff --git a/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean b/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean index 0a996e925745b1..f3f9d6131ba33e 100644 --- a/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean +++ b/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean @@ -296,7 +296,7 @@ functions `f : M → N` is `C^n` whenever the denominator is non-zero. section Div variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} -{H : Type*} [TopologicalSpace H] {E : Type*} + {H : Type*} [TopologicalSpace H] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean index ad79b077cc3151..e66aca913c596c 100644 --- a/Mathlib/MeasureTheory/Measure/AddContent.lean +++ b/Mathlib/MeasureTheory/Measure/AddContent.lean @@ -68,7 +68,7 @@ open scoped ENNReal Topology Function namespace MeasureTheory variable {α : Type*} {C : Set (Set α)} {s t : Set α} {I : Finset (Set α)} -{G : Type*} [AddCommMonoid G] + {G : Type*} [AddCommMonoid G] variable (G) in /-- An additive content is a set function with value 0 at the empty set which is finitely additive diff --git a/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean b/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean index b296f2ba2d867e..1b2399ac8c7fd0 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean @@ -27,7 +27,7 @@ open scoped symmDiff namespace MeasureTheory.VectorMeasure variable {α : Type*} {hα : MeasurableSpace α} {E : Type*} [NormedAddCommGroup E] -[CompleteSpace E] {μ : Measure α} + [CompleteSpace E] {μ : Measure α} /-- A finitely additive vector measure which is dominated by a finite positive measure is in fact countably additive. -/ diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index 8cde123aca73ac..84672e45cd0ccc 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -421,18 +421,18 @@ If infinitely many of the `Rᵢ` are nontrivial, then there exists an ideal of ` is not of the form `Πᵢ Iᵢ`, namely the ideal of finitely supported elements of `Πᵢ Rᵢ` (it is also not a principal ideal).) -/ @[simps!] def piOrderIso [Finite ι] : Ideal (Π i, R i) ≃o Π i, Ideal (R i) := .symm -{ toFun := pi - invFun I i := I.map (Pi.evalRingHom R i) - left_inv _ := funext map_evalRingHom_pi - right_inv I := by - ext r - simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)] - refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩ - have := Fintype.ofFinite ι - classical rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by - rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp] - exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1 - map_rel_iff' := pi_le_pi_iff } + { toFun := pi + invFun I i := I.map (Pi.evalRingHom R i) + left_inv _ := funext map_evalRingHom_pi + right_inv I := by + ext r + simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)] + refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩ + have := Fintype.ofFinite ι + classical rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by + rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp] + exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1 + map_rel_iff' := pi_le_pi_iff } instance [Finite ι] [∀ i, IsPrincipalIdealRing (R i)] : IsPrincipalIdealRing (Π i, R i) where principal I := by From 7845a1a8a89d4866c945495019d281ecbe50c454 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Apr 2026 18:40:47 +0000 Subject: [PATCH 12/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index bd012465e8def1..7ac1d0e130f7f7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c0286d9a17937d9e498f0bb3c499d97eceb05ba9", + "rev": "645e49d5f6a3b43d21cbdbd0484181cecc085e6e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13229", diff --git a/lean-toolchain b/lean-toolchain index 5f005db8ca8aa7..1ea9ba3f8c011f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13229-f76c89f +leanprover/lean4-pr-releases:pr-release-13229-bc5b0e2 From 7eff8163b61dac77cb19660fa7b4354eddabe274 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Apr 2026 20:26:29 +0000 Subject: [PATCH 13/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13223 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c668987c11650a..5ab4eaacb44520 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3d5a3aaab3de9235f10521681974f5043f072f09", + "rev": "a2574fe95a9b75fc8a5704154115a2a1b1772fcb", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13223", diff --git a/lean-toolchain b/lean-toolchain index 30316b1566a727..5079d14de1510d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13223-f92b7f3 +leanprover/lean4-pr-releases:pr-release-13223-4d67b4b From e533fdeaf038eb1c7a142de54952aaa4f13a7b86 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Apr 2026 20:54:17 +0000 Subject: [PATCH 14/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7ac1d0e130f7f7..4968304ce962ff 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "645e49d5f6a3b43d21cbdbd0484181cecc085e6e", + "rev": "21b86a5d3de7134e36ad9372b10db4ebe6537191", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13229", diff --git a/lean-toolchain b/lean-toolchain index 1ea9ba3f8c011f..69c3d1e0bc8491 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13229-bc5b0e2 +leanprover/lean4-pr-releases:pr-release-13229-626213b From 37ec501598b2e669c96887b98772955a401c8df2 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Apr 2026 21:51:50 +0000 Subject: [PATCH 15/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 4968304ce962ff..b21529f793d4ee 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "21b86a5d3de7134e36ad9372b10db4ebe6537191", + "rev": "6c58796406bf6d10afc8514df1595148a731926f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13229", diff --git a/lean-toolchain b/lean-toolchain index 69c3d1e0bc8491..916fc0e7235449 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13229-626213b +leanprover/lean4-pr-releases:pr-release-13229-0fc6e49 From 3602bc00f4e3fb51998e120ca7d3ff64568e0150 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 2 Apr 2026 09:47:36 +0000 Subject: [PATCH 16/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b21529f793d4ee..089d82ac330bf7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6c58796406bf6d10afc8514df1595148a731926f", + "rev": "7c36ea46afccf4a11da46b6faae490f5cf4a3043", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13229", diff --git a/lean-toolchain b/lean-toolchain index 916fc0e7235449..b6747cfdc39309 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13229-0fc6e49 +leanprover/lean4-pr-releases:pr-release-13229-aa77588 From ce608e72cea947a87d76f86f5583c60d3f2a3853 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 2 Apr 2026 12:30:02 +0000 Subject: [PATCH 17/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13223 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 3a486d56d4b24e..fc6693b09cc150 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9e1475e92dfb360d79e99735fdae80e5831aa6c6", + "rev": "4b683d8a24a7cac230de80594e886e5457abc842", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13223", diff --git a/lean-toolchain b/lean-toolchain index 16cbaa6b60163f..34303e5e753d6e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13223-59d9492 +leanprover/lean4-pr-releases:pr-release-13223-e72d42c From f8c6bd6ecd104f93ca754ca7e5a7de6f7af11698 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 2 Apr 2026 14:16:34 +0000 Subject: [PATCH 18/77] chore: fix linter tests --- MathlibTest/LintStyle.lean | 4 ---- MathlibTest/globalAttributeIn.lean | 37 ++++-------------------------- 2 files changed, 5 insertions(+), 36 deletions(-) diff --git a/MathlibTest/LintStyle.lean b/MathlibTest/LintStyle.lean index 28ac686c00c5ce..6783965170584b 100644 --- a/MathlibTest/LintStyle.lean +++ b/MathlibTest/LintStyle.lean @@ -201,7 +201,6 @@ set_option linter.style.cdot true set_option allowUnsafeReducibility true in attribute [instance_reducible] Int.add -set_option linter.globalAttributeIn false in /-- warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'. @@ -216,7 +215,6 @@ warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'. Note: This linter can be disabled with `set_option linter.style.cdot false` -/ #guard_msgs in -attribute [instance] Int.add in instance : Inhabited Nat where default := by . have := 0 @@ -276,7 +274,6 @@ example : True := by end cdotLinter set_option linter.style.dollarSyntax true -set_option linter.globalAttributeIn false in /-- warning: Please use '<|' instead of '$' for the pipe operator. @@ -287,7 +284,6 @@ warning: Please use '<|' instead of '$' for the pipe operator. Note: This linter can be disabled with `set_option linter.style.dollarSyntax false` -/ #guard_msgs in -attribute [instance] Int.add in instance (f g : Nat → Nat) : Inhabited Nat where default := by · have := 0 diff --git a/MathlibTest/globalAttributeIn.lean b/MathlibTest/globalAttributeIn.lean index 37f273b69bc93b..a61961950ef7e2 100644 --- a/MathlibTest/globalAttributeIn.lean +++ b/MathlibTest/globalAttributeIn.lean @@ -8,33 +8,14 @@ import Mathlib.Tactic.Linter.GlobalAttributeIn /-! Tests for the `globalAttributeIn` linter. -/ --- Test disabling the linter. -set_option linter.globalAttributeIn false - -- After https://github.com/leanprover/lean4/pull/12263, -- we need to add `instance_reducible` before we can add `instance` to `Int.add`. set_option allowUnsafeReducibility true in attribute [instance_reducible] Int.add -set_option autoImplicit false in -attribute [instance] Int.add in -instance : Inhabited Int where - default := 0 - -set_option linter.globalAttributeIn true - -set_option linter.globalAttributeIn false in -attribute [instance] Int.add in -instance : Inhabited Int where - default := 0 - --- Global instances with `in`, are linted, as they are a footgun. - /-- -warning: Despite the `in`, the attribute 'instance 1100' is added globally to 'Int.add' +error: Despite the `in`, the attribute instance 1100 is added globally to Int.add please remove the `in` or make this a `local instance 1100` - -Note: This linter can be disabled with `set_option linter.globalAttributeIn false` -/ #guard_msgs in set_option autoImplicit false in @@ -44,10 +25,8 @@ instance : Inhabited Int where default := 0 /-- -warning: Despite the `in`, the attribute 'instance' is added globally to 'Int.add' +error: Despite the `in`, the attribute instance is added globally to Int.add please remove the `in` or make this a `local instance` - -Note: This linter can be disabled with `set_option linter.globalAttributeIn false` -/ #guard_msgs in attribute [instance] Int.add in @@ -55,10 +34,8 @@ instance : Inhabited Int where default := 0 /-- -warning: Despite the `in`, the attribute 'simp' is added globally to 'Int.add' +error: Despite the `in`, the attribute simp is added globally to Int.add please remove the `in` or make this a `local simp` - -Note: This linter can be disabled with `set_option linter.globalAttributeIn false` -/ #guard_msgs in attribute [simp] Int.add in @@ -73,15 +50,11 @@ namespace X theorem foo (x y : Nat) : x = y := sorry /-- -warning: Despite the `in`, the attribute 'simp' is added globally to 'foo' +error: Despite the `in`, the attribute simp is added globally to foo please remove the `in` or make this a `local simp` - -Note: This linter can be disabled with `set_option linter.globalAttributeIn false` --- -warning: Despite the `in`, the attribute 'ext' is added globally to 'foo' +error: Despite the `in`, the attribute ext is added globally to foo please remove the `in` or make this a `local ext` - -Note: This linter can be disabled with `set_option linter.globalAttributeIn false` -/ #guard_msgs in attribute [simp, local simp, ext, scoped instance, -simp, -ext] foo in From 8d08e270ece92c1a812fbbca183872691c19f542 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 14:35:06 +1000 Subject: [PATCH 19/77] lake update --- lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index dfad1f83a0b0fd..ca0e4c0d66b879 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -45,20 +45,20 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21", + "rev": "ad416ddf6cc9d5b1c00eaf04a48e703538132760", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "nightly-testing", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057", + "rev": "bee778191c7fbea31864ecfe1809b8837626aba0", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "nightly-testing", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", diff --git a/lakefile.lean b/lakefile.lean index e22e0ef045be20..5f11ec894a69ad 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,8 +7,8 @@ open Lake DSL -/ require "leanprover-community" / "batteries" @ git "v4.30.0-rc1" -require "leanprover-community" / "Qq" @ git "v4.30.0-rc1" -require "leanprover-community" / "aesop" @ git "v4.30.0-rc1" +require "leanprover-community" / "Qq" @ git "nightly-testing" +require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.97" with NameMap.empty.insert `errorOnBuild "ProofWidgets failed to reuse pre-built JS code. \ From 940f396db97c9c3cd13cc116ab54384a3212a5d3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 14:36:04 +1000 Subject: [PATCH 20/77] fix hash command linter --- Mathlib/Tactic/Linter/HashCommandLinter.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index 3f2c8f926bef0b..c8b650c5c99d36 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -49,7 +49,7 @@ Intended to be used in the `hashCommand` linter, where we want to enter `set_opt private partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun stx => do if stx.getKind == ``Lean.Parser.Command.in then if stx[0].getKind == ``Lean.Parser.Command.set_option then - let opts ← Elab.elabSetOption stx[0][1] stx[0][3] + let (opts, _) ← Elab.elabSetOption stx[0][1] stx[0][3] withScope (fun scope => { scope with opts }) do withSetOptionIn' cmd stx[2] else From 12400c59a92b6fbfe39d0f04b6056428bcfea3d8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 14:47:54 +1000 Subject: [PATCH 21/77] fix bad merge --- Mathlib/Computability/Partrec.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Mathlib/Computability/Partrec.lean b/Mathlib/Computability/Partrec.lean index 5e1ef4c6b9fcfb..c8363e6f90b16b 100644 --- a/Mathlib/Computability/Partrec.lean +++ b/Mathlib/Computability/Partrec.lean @@ -718,9 +718,6 @@ theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) : b ∈ PFun.fix f a := by intro F; refine ⟨fun h => ?_, fun h => ?_⟩ · rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩ - #adaptation_note /-- Before leanprover/lean4#13166, the proof from here to the end of the - first branch was: - ``` have : ∀ m a', Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a := by intro m a' am ba induction m generalizing a' with simp [F] at am @@ -754,9 +751,9 @@ theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) : · simpa [F] using Or.inr ⟨_, hk, h₂⟩ · rwa [le_antisymm (Nat.le_of_lt_succ mk) km] · rcases IH _ am₃ k.succ (by simpa [F] using ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩ - #adaptation_note /-- After leanprover/lean4#13166 which arrived in nightly-2026-03-28: - This `clear_value` used to not be necessary. - -/ + #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166 + (replacing grind's canonicalizer with a type-directed normalizer), + the `clear_value F` was not required here. -/ clear_value F grind From 89270ab2e3ca65c4b99cb3a658159630b6cc9d13 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 15:14:26 +1000 Subject: [PATCH 22/77] fixes --- .../Analysis/SpecialFunctions/Pow/NthRootLemmas.lean | 11 +++++++++++ Mathlib/NumberTheory/Padics/MahlerBasis.lean | 4 ++-- Mathlib/RingTheory/Smooth/Local.lean | 9 ++++++++- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean | 4 +++- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean | 8 ++++++-- 5 files changed, 30 insertions(+), 6 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean index eac12117d3ea82..2f2b7c12bcd278 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean @@ -64,9 +64,20 @@ private theorem nthRoot.lt_pow_go_succ_aux0 (hb : b ≠ 0) : rw [Nat.le_div_iff_mul_le (by positivity), Nat.mul_comm, ← Nat.add_mul_div_right _ _ (by positivity), Nat.le_div_iff_mul_le (by positivity)] + #adaptation_note /-- Prior to nightly-2026-04-06, this was + ``` have := (Commute.all (b : ℤ) (a - b)).pow_add_mul_le_add_pow_of_sq_nonneg (by positivity) (sq_nonneg _) (sq_nonneg _) (by grind) (n + 1) grind + ``` + -/ + zify + have h := pow_add_mul_le_add_pow_of_sq_nonneg (a := (b : ℤ)) (b := (a : ℤ) - b) + (ha := by positivity) (Hsq := by positivity) (Hsq' := by positivity) (H := by omega) + (n := n + 1) + rw [← sub_nonneg] at h ⊢ + convert h using 1 + rw [pow_succ]; push_cast; ring1 private theorem nthRoot.always_exists (n a : ℕ) : ∃ c, c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1) := by diff --git a/Mathlib/NumberTheory/Padics/MahlerBasis.lean b/Mathlib/NumberTheory/Padics/MahlerBasis.lean index a0916015af130c..16a262245746ed 100644 --- a/Mathlib/NumberTheory/Padics/MahlerBasis.lean +++ b/Mathlib/NumberTheory/Padics/MahlerBasis.lean @@ -176,12 +176,12 @@ private lemma bojanic_mahler_step2 {f : C(ℤ_[p], E)} {s t : ℕ} refine (nnnorm_smul_le _ _).trans <| mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le]) -- remains to show norm of binomial coeff is `≤ p⁻¹` rw [mem_range] at hi - have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by lia) + have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by omega) rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, PadicInt.norm_eq_zpow_neg_valuation (mod_cast this.ne'), coe_zpow, NNReal.coe_natCast, zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt), neg_le_neg_iff, ← PadicInt.valuation_coe, PadicInt.coe_natCast, Padic.valuation_natCast, Nat.one_le_cast] - exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by lia) + exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by omega) · -- Bounding the sum over `range (n + 1)`: every term is small by the choice of `t` refine norm_sum_le_of_forall_le_of_nonempty nonempty_range_add_one (fun i _ ↦ ?_) calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖ diff --git a/Mathlib/RingTheory/Smooth/Local.lean b/Mathlib/RingTheory/Smooth/Local.lean index 1170568f1a0884..e5b65c1c483373 100644 --- a/Mathlib/RingTheory/Smooth/Local.lean +++ b/Mathlib/RingTheory/Smooth/Local.lean @@ -86,7 +86,14 @@ theorem FormallySmooth.iff_injective_cotangentComplexBaseChange (cotangentComplexBaseChange R S P (ResidueField S)).baseChange K ∘ₗ (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.toLinearMap = (cotangentComplexBaseChange R S P K) := by - ext; simp [cotangentComplexBaseChange_tmul] + ext + #adaptation_note /-- Prior to nightly-2026-04-06, this was just `simp`. -/ + simp_rw [AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_comp, curry_apply, + LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, Function.comp_apply, + AlgebraTensorModule.cancelBaseChange_symm_tmul, LinearMap.baseChange_tmul, + cotangentComplexBaseChange_tmul, kerToTensor_apply, one_smul] + erw [AlgebraTensorModule.cancelBaseChange_tmul] + simp rw [← this] refine .trans ?_ ((AlgebraTensorModule.cancelBaseChange _ _ _ _ _).comp_injective _).symm exact ((AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.injective_comp _).symm diff --git a/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean b/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean index 116668a97005d1..f18305d1ebe4a1 100644 --- a/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean +++ b/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean @@ -363,6 +363,8 @@ lemma rankAtStalk_eq (p : PrimeSpectrum R) : let e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M := AlgebraTensorModule.cancelBaseChange _ _ _ _ _ - rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct] + rw [← e.finrank_eq] + erw [finrank_baseChange] + rw [rankAtStalk_eq_finrank_tensorProduct] end Module diff --git a/Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean b/Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean index 69e1acf489083f..47857e62d8d4bf 100644 --- a/Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean +++ b/Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean @@ -45,13 +45,16 @@ lemma isNilpotent_tensor_residueField_iff · have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0] have : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A := by - rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul] + rw [Module.finrank_tensorProduct] + erw [Module.finrank_self] + rw [one_mul] rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective] simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, Algebra.coe_lmul_eq_mul, Algebra.TensorProduct.comm_tmul] rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)), LinearMap.isNilpotent_iff_charpoly, ← Algebra.baseChange_lmul, LinearMap.charpoly_baseChange] - simp_rw [this, ← ((LinearMap.mul R A) f).charpoly_natDegree] + erw [this] + simp_rw [← ((LinearMap.mul R A) f).charpoly_natDegree] constructor · intro e i hi replace e := congr(($e).coeff i) @@ -137,6 +140,7 @@ end PrimeSpectrum namespace Polynomial +set_option backward.isDefEq.respectTransparency false in lemma mem_image_comap_C_basicOpen (f : R[X]) (x : PrimeSpectrum R) : x ∈ comap C '' basicOpen f ↔ ∃ i, f.coeff i ∉ x.asIdeal := by trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0 From c102fda895612f50316183af35ee8621658a3fd3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 15:46:54 +1000 Subject: [PATCH 23/77] fixes --- .../Rpow/RingInverseOrder.lean | 20 ++++++++++++++++--- .../EisensteinSeries/E2/Transform.lean | 2 +- .../LocalRing/ResidueField/Polynomial.lean | 4 +++- .../RingTheory/Unramified/LocalStructure.lean | 5 +++++ 4 files changed, 26 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean index 95d298facbfa5c..11025531a88a4e 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean @@ -48,12 +48,22 @@ public lemma convexOn_ringInverse : by_cases ha' : a = 0 · have hb' : b = 1 := by grind simp only [ha', hb', one_mul, zero_add, gt_iff_lt] - grind + #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. + `spectrum_pos` is not activating in `grind` despite the + ``` + grind_pattern IsStrictlyPositive.spectrum_pos => x ∈ spectrum 𝕜 a, IsStrictlyPositive a + ``` + rule, because `grind` will not fill in the `𝕜 := ℝ`. -/ + exact zpos.spectrum_pos hr · grind [add_pos_of_pos_of_nonneg, mul_nonneg] have h₂ : (a • 1 + b • z ^ (-1 : ℝ)) = cfc (fun r => (a + b * r ^ (-1 : ℝ))) z := by rw [CFC.rpow_eq_cfc_real zpos.nonneg] have hcont : ContinuousOn (fun r : ℝ => (r ^ (-1 : ℝ))) (spectrum ℝ z) := - ContinuousOn.rpow_const (f := id) (by fun_prop) (by grind) + ContinuousOn.rpow_const (f := id) (by fun_prop) (by + #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/ + intro x h + have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h + grind) rw [← cfc_smul b _ z hcont, ← Algebra.algebraMap_eq_smul_one, ← cfc_const_add a _ z] refine cfc_congr fun r hr => ?_ simp @@ -72,7 +82,11 @@ public lemma convexOn_ringInverse : have : 0 ≤ b * r := by positivity cases lt_or_eq_of_le ha <;> grind · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _ - exact ContinuousOn.rpow_const (by fun_prop) (by grind) + exact ContinuousOn.rpow_const (by fun_prop) (by + #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/ + intro x h + have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h + grind) · intro r hr suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by simp_rw [← Real.rpow_intCast] at this diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean index 771eae90dacbbc..2eeb0a33fcee3b 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean +++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean @@ -136,7 +136,7 @@ lemma G2_eq_tsum_G2Term (z : ℍ) : G2 z = ∑' m, ∑' n, G2Term z ![m, n] := b exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat]) · simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero] using (G2Term_prod_summable z).prod - · grind [(G2Term_prod_summable z).prod.congr] + · exact (G2Term_prod_summable z).prod · exact summable_zero.congr fun b ↦ by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b] diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean index 671dd76bf0d9e9..f73500b01275f0 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean +++ b/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean @@ -60,7 +60,9 @@ def residueFieldMapCAlgEquiv [J.LiesOver I] (hJ : J = I.map C) : apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr simpa [hx, aeval_map_algebraMap, aeval_algebraMap_apply, Algebra.smul_def] using hr refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_ - simp only [← algebraMap_eq, ← Algebra.smul_def, algebraMap_smul, ← hr] + simp only [← algebraMap_eq, ← Algebra.smul_def] + erw [algebraMap_smul] + simp only [← hr] simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using hJ.le hx · apply AlgHom.coe_ringHom_injective apply IsFractionRing.injective_comp_algebraMap (A := I.ResidueField[X]) diff --git a/Mathlib/RingTheory/Unramified/LocalStructure.lean b/Mathlib/RingTheory/Unramified/LocalStructure.lean index 8addca99368585..5f5b483d59f010 100644 --- a/Mathlib/RingTheory/Unramified/LocalStructure.lean +++ b/Mathlib/RingTheory/Unramified/LocalStructure.lean @@ -209,6 +209,11 @@ lemma exists_notMem_forall_ne_mem_and_adjoin_eq_top #adaptation_note /-- Needed after nightly-2023-02-23 -/ have : p.IsPrime := Ideal.IsPrime.under R Q classical + #adaptation_note /-- After nightly-2026-04-06, typeclass synthesis fails to find these + instances; provide them explicitly. -/ + letI : Module p.ResidueField (p.Fiber S) := TensorProduct.leftModule + letI : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right + letI : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S have : IsArtinianRing (p.Fiber S) := .of_finite p.ResidueField _ let α := PrimeSpectrum.primesOverOrderIsoFiber R S p obtain ⟨x, hx0, hx⟩ : ∃ x : Q.ResidueField, x ≠ 0 ∧ p.ResidueField[x] = ⊤ := by From 3a751b4e712416f981239ca850d8bed38f9a0269 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 16:28:08 +1000 Subject: [PATCH 24/77] unpleasant fix. --- .../Trigonometric/Chebyshev/RootsExtrema.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean index 0eee892dbf77bd..92a5f70d0bf6dd 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean @@ -44,7 +44,15 @@ theorem eval_T_real_mem_Icc (n : ℤ) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : grind [T_real_cos, cos_mem_Icc] theorem abs_eval_T_real_le_one (n : ℤ) {x : ℝ} (hx : |x| ≤ 1) : - |(T ℝ n).eval x| ≤ 1 := by grind [eval_T_real_mem_Icc] + |(T ℝ n).eval x| ≤ 1 := by + #adaptation_note /-- Before nightly-2026-04-07, this was just + `grind [eval_T_real_mem_Icc]`. `grind`'s e-matching now keeps the + `Polynomial.eval` produced by the lemma (which uses `instCommSemiring.toSemiring`) + and the `Polynomial.eval` propagated by abs unfolding (which uses `Real.semiring`) + as distinct atoms, even though they are `rfl`-equal, so the contradiction is + never found. -/ + have h := eval_T_real_mem_Icc n (Set.mem_Icc.mpr (abs_le.mp hx)) + exact abs_le.mpr (Set.mem_Icc.mp h) theorem one_le_eval_T_real (n : ℤ) {x : ℝ} (hx : 1 ≤ x) : 1 ≤ (T ℝ n).eval x := by rw [← cosh_arcosh hx] From 5212dc478426d5caca02fc5aea6df6d211fbdd7e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 17:16:19 +1000 Subject: [PATCH 25/77] touch for CI From ac5cf06a1486851b71217ca2e627eb652b6801a9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 18:26:03 +1000 Subject: [PATCH 26/77] cleanup of adaptation notes --- Mathlib/Algebra/Group/Ext.lean | 6 +----- Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean | 6 +----- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 6 +----- Mathlib/Data/Fin/VecNotation.lean | 3 +-- Mathlib/Data/Matrix/Reflection.lean | 4 ---- 5 files changed, 4 insertions(+), 21 deletions(-) diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean index 4de2994db58ed2..3874fa32780c75 100644 --- a/Mathlib/Algebra/Group/Ext.lean +++ b/Mathlib/Algebra/Group/Ext.lean @@ -109,11 +109,7 @@ theorem CancelMonoid.toRightCancelMonoid_injective {M : Type u} : theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} : Function.Injective (@CancelCommMonoid.toCommMonoid M) := by rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h - #adaptation_note /-- Before leanprover/lean4#13166, the last line was `grind`. - The new type-directed canonicalizer tries to synthesize `Monoid M` / `CommMonoid M` to normalize - sub-expressions, but fails because after `rintro` the instances exist only as destructured fields - in the local context, not as registered typeclass instances. -/ - cases h; rfl + grind @[to_additive (attr := ext)] theorem CancelCommMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄ diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean index 30e04adcabb923..fbe99b3892ded6 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean @@ -331,11 +331,7 @@ theorem integral_cos_mul_complex {z : ℂ} (hz : z ≠ 0) (a b : ℝ) : have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _ have c : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b have d := HasDerivAt.comp_ofReal (c.div_const z) - #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166 - (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal. - It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new - canonicalizer; a minimization would help. The original proof was: `grind` -/ - simpa [hz, mul_comm] using d + grind theorem integral_cos_sq_sub_sin_sq : ∫ x in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index a8976fcfe16ed7..a9491a78f72c6f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean @@ -652,11 +652,7 @@ lemma exists_isCycle_of_two_le_isEdgeReachable {u v : V} (huv : u ≠ v) {n : (h : G.IsEdgeReachable n u v) : ∃ w : G.Walk u u, w.IsCycle := by classical obtain ⟨w, hw, h⟩ := exists_adj_isEdgeReachable_two huv (h.anti hn) - #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166 - (replacing grind's canonicalizer with a type-directed normalizer), this was just - `have := @h {s(u, w)} (by simp)`. It is not yet clear whether this is due to defeq abuse in - Mathlib or a problem in the new canonicalizer; a minimization would help. -/ - have := @h {s(u, w)} (by simp only [Set.encard_singleton, Nat.cast_ofNat]; decide) + have := @h {s(u, w)} (by simp) obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩ exact ⟨p.rotate _ (p.fst_mem_support_of_mem_edges hp₂), hp₁.rotate _⟩ diff --git a/Mathlib/Data/Fin/VecNotation.lean b/Mathlib/Data/Fin/VecNotation.lean index 9da254a61f272d..11479cbb45ed13 100644 --- a/Mathlib/Data/Fin/VecNotation.lean +++ b/Mathlib/Data/Fin/VecNotation.lean @@ -413,8 +413,7 @@ theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) : simp only [Nat.mod_add_mod, Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)] refine (Nat.mod_eq_of_lt ?_).symm - #adaptation_note /-- After leanprover/lean4#13166, the `lia` tactic was timing out here. -/ - omega + lia @[simp] theorem vecHead_vecAlt0 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : diff --git a/Mathlib/Data/Matrix/Reflection.lean b/Mathlib/Data/Matrix/Reflection.lean index 6e45ce70128528..2c82f38918ffcc 100644 --- a/Mathlib/Data/Matrix/Reflection.lean +++ b/Mathlib/Data/Matrix/Reflection.lean @@ -207,10 +207,6 @@ example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b def etaExpand {m n} (A : Matrix (Fin m) (Fin n) α) : Matrix (Fin m) (Fin n) α := Matrix.of (FinVec.etaExpand fun i => FinVec.etaExpand fun j => A i j) -#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166 -(replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal. -It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new -canonicalizer; a minimization would help. The original proof was: `grind` -/ /-- This can be used to prove ```lean example (A : Matrix (Fin 2) (Fin 2) α) : From 85c19f239fc3a167a10e676314e00d305d2d4df9 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Tue, 7 Apr 2026 08:32:32 +0000 Subject: [PATCH 27/77] chore: adaptations for nightly-2026-04-06 From 939b2837a108267d255e41aece8c6aca29009a2a Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Tue, 7 Apr 2026 11:42:14 +0000 Subject: [PATCH 28/77] chore: bump to nightly-2026-04-07 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 845eced439d5e8..54caac41bddf21 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-06 +leanprover/lean4:nightly-2026-04-07 From fc6fe78b86732d20548064bc16550db6f1781c50 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Tue, 7 Apr 2026 12:52:43 +0000 Subject: [PATCH 29/77] chore: adaptations for nightly-2026-04-07 From 177922a8f8c95f77b3ed570eec55c8dea76dff27 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Wed, 8 Apr 2026 09:32:09 +0000 Subject: [PATCH 30/77] chore: bump to nightly-2026-04-08 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 54caac41bddf21..e33d600a6f3af0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-07 +leanprover/lean4:nightly-2026-04-08 From 9e49d8cb9a70a2add52730fb5f7b46561cfa53d6 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 8 Apr 2026 17:58:27 +0000 Subject: [PATCH 31/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13262 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index ca0e4c0d66b879..65350d7df7920a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bf597c77bf9b8e66720d724928207f5911533113", + "rev": "8043da856f876ee8095e8ed7da98c7a461f0095b", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "lean-pr-testing-13262", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 5f11ec894a69ad..ec9eb91e3274a1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "v4.30.0-rc1" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-13262" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.97" diff --git a/lean-toolchain b/lean-toolchain index 54caac41bddf21..48e83f3fea7ef9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-07 +leanprover/lean4-pr-releases:pr-release-13262-880d558 From 6cc8eafaec204db7f77bb679aa747d52544a2a35 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 8 Apr 2026 23:55:25 +0000 Subject: [PATCH 32/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13262 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 65350d7df7920a..f696af530ecb8d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8043da856f876ee8095e8ed7da98c7a461f0095b", + "rev": "81df6fddd38f4325480fed81241ffc8a362e3143", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13262", diff --git a/lean-toolchain b/lean-toolchain index 48e83f3fea7ef9..d2fd232933faf2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13262-880d558 +leanprover/lean4-pr-releases:pr-release-13262-3d078ba From 8335db377cca76d18420cf00e36c98854d87404b Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 8 Apr 2026 20:25:06 -0700 Subject: [PATCH 33/77] universe fixes --- Mathlib/CategoryTheory/Sites/Sheaf.lean | 4 ++-- Mathlib/CategoryTheory/Sites/Sieves.lean | 6 +++--- Mathlib/CategoryTheory/Types/Basic.lean | 2 +- Mathlib/CategoryTheory/Yoneda.lean | 8 ++++---- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean index df2d7918806dde..9df8cd42462f17 100644 --- a/Mathlib/CategoryTheory/Sites/Sheaf.lean +++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean @@ -353,7 +353,7 @@ abbrev Sheaf.homEquiv {X Y : Sheaf J A} : (X ⟶ Y) ≃ (X.obj ⟶ Y.obj) := def sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf : sheafToPresheaf J A ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (sheafToPresheaf J A).op ≅ yoneda := - Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftYonedaIsoYoneda.symm.{max u₁ v₂} _) ≪≫ + Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftYonedaIsoYoneda.{max u₁ v₂}.symm _) ≪≫ (fullyFaithfulSheafToPresheaf J A).compUliftYonedaCompWhiskeringLeft ≪≫ uliftYonedaIsoYoneda @@ -368,7 +368,7 @@ def sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf : (sheafToPresheaf J A).op ⋙ coyoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (sheafToPresheaf J A) ≅ coyoneda := - Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftCoyonedaIsoCoyoneda.symm.{max u₁ v₂} _) ≪≫ + Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftCoyonedaIsoCoyoneda.{max u₁ v₂}.symm _) ≪≫ (fullyFaithfulSheafToPresheaf J A).compUliftCoyonedaCompWhiskeringLeft ≪≫ uliftCoyonedaIsoCoyoneda diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index 1a8c94931b14ec..940d06cd77b668 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/Mathlib/CategoryTheory/Sites/Sieves.lean @@ -1253,13 +1253,13 @@ def uliftNatTransOfLe {S T : Sieve X} (h : S ≤ T) : /-- A variant of `Sieve.functorInclusion` with universe lifting. -/ @[simps! app] def uliftFunctorInclusion (S : Sieve X) : - S.uliftFunctor ⟶ uliftYoneda.obj.{w} X := + S.uliftFunctor ⟶ uliftYoneda.{w}.obj X := Functor.whiskerRight S.functorInclusion CategoryTheory.uliftFunctor /-- A variant of `Sieve.toFunctor` with universe lifting. -/ @[simps] def toUliftFunctor (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S f) : - uliftYoneda.obj.{w} Y ⟶ Sieve.uliftFunctor.{w} S where + uliftYoneda.{w}.obj Y ⟶ Sieve.uliftFunctor.{w} S where app Z g := ⟨g.down ≫ f, S.downward_closed hf g.down⟩ theorem uliftNatTransOfLe_comm {S T : Sieve X} (h : S ≤ T) : @@ -1276,7 +1276,7 @@ instance uliftFunctorInclusion_is_mono (S : Sieve X) : /-- A variant of `Sieve.sieveOfSubfunctor` with universe lifting. -/ @[simps] -def sieveOfUliftSubfunctor {R : Cᵒᵖ ⥤ Type max w v₁} (f : R ⟶ uliftYoneda.obj.{w} X) : +def sieveOfUliftSubfunctor {R : Cᵒᵖ ⥤ Type max w v₁} (f : R ⟶ uliftYoneda.{w}.obj X) : Sieve X where arrows Y g := ∃ t, f.app (Opposite.op Y) t = { down := g } downward_closed := by diff --git a/Mathlib/CategoryTheory/Types/Basic.lean b/Mathlib/CategoryTheory/Types/Basic.lean index b2eb9a5f8f913a..87b829cfad9285 100644 --- a/Mathlib/CategoryTheory/Types/Basic.lean +++ b/Mathlib/CategoryTheory/Types/Basic.lean @@ -204,7 +204,7 @@ def uliftFunctor : Type u ⥤ Type max u v where map {X} {_} f := fun x : ULift.{v} X => ULift.up (f x.down) @[simp] -theorem uliftFunctor_obj {X : Type u} : uliftFunctor.obj.{v} X = ULift.{v} X := +theorem uliftFunctor_obj {X : Type u} : uliftFunctor.{v}.obj X = ULift.{v} X := rfl @[simp] diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean index d4afb27182601d..208d8ba2ce4e48 100644 --- a/Mathlib/CategoryTheory/Yoneda.lean +++ b/Mathlib/CategoryTheory/Yoneda.lean @@ -1245,7 +1245,7 @@ variable {C : Type u₁} [Category.{v₁} C] /-- `FullyFaithful.homEquiv` as a natural isomorphism. -/ @[simps!] def homNatIso {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) : - F.op ⋙ uliftYoneda.obj.{v₁} (F.obj X) ≅ uliftYoneda.obj.{v₂} X := + F.op ⋙ uliftYoneda.{v₁}.obj (F.obj X) ≅ uliftYoneda.{v₂}.obj X := NatIso.ofComponents (fun Y => Equiv.toIso (Equiv.ulift.trans <| hF.homEquiv.symm.trans Equiv.ulift.symm)) (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))) @@ -1253,7 +1253,7 @@ def homNatIso {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFai /-- `FullyFaithful.homEquiv` as a natural isomorphism. -/ @[simps!, deprecated homNatIso (since := "2025-10-28")] def homNatIsoMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) - (X : C) : F.op ⋙ yoneda.obj (F.obj X) ≅ uliftYoneda.obj.{v₂} X := + (X : C) : F.op ⋙ yoneda.obj (F.obj X) ≅ uliftYoneda.{v₂}.obj X := isoWhiskerLeft F.op (uliftYonedaIsoYoneda.symm.app _) ≪≫ hF.homNatIso _ ≪≫ NatIso.ofComponents (fun _ => Equiv.toIso (Equiv.ulift.trans Equiv.ulift.symm)) @@ -1273,7 +1273,7 @@ def compUliftYonedaCompWhiskeringLeft {D : Type u₂} [Category.{v₂} D] {F : C @[simps!, deprecated compUliftYonedaCompWhiskeringLeft (since := "2025-10-28")] def compYonedaCompWhiskeringLeftMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) : F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ≅ uliftYoneda.{v₂} := by - refine isoWhiskerLeft F (isoWhiskerRight uliftYonedaIsoYoneda.symm.{v₁} _) ≪≫ + refine isoWhiskerLeft F (isoWhiskerRight uliftYonedaIsoYoneda.{v₁}.symm _) ≪≫ hF.compUliftYonedaCompWhiskeringLeft ≪≫ NatIso.ofComponents (fun _ => NatIso.ofComponents (fun _ => Equiv.toIso (Equiv.ulift.trans Equiv.ulift.symm))) @@ -1281,7 +1281,7 @@ def compYonedaCompWhiskeringLeftMaxRight {D : Type u₂} [Category.{max v₁ v /-- `FullyFaithful.homEquiv` as a natural isomorphism, using coyoneda. -/ @[simps!] def homNatIso' {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) : - F ⋙ uliftCoyoneda.obj.{v₁} (op (F.obj X)) ≅ uliftCoyoneda.obj.{v₂} (op X) := + F ⋙ uliftCoyoneda.{v₁}.obj (op (F.obj X)) ≅ uliftCoyoneda.{v₂}.obj (op X) := NatIso.ofComponents (fun Y => Equiv.toIso (Equiv.ulift.trans <| hF.homEquiv.symm.trans Equiv.ulift.symm)) (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))) From ba688b059328e6c04ee9dd81d14b02118c1bd202 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Thu, 9 Apr 2026 09:23:23 +0000 Subject: [PATCH 34/77] chore: bump to nightly-2026-04-09 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index e33d600a6f3af0..d04b8570d780a2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-08 +leanprover/lean4:nightly-2026-04-09 From 5c03f00b1b90ad5cd6855e50502e6dd8800365ee Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Apr 2026 02:21:15 +0000 Subject: [PATCH 35/77] lake update --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index f159f5ea44360d..e1195bfea169f7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bf597c77bf9b8e66720d724928207f5911533113", + "rev": "e32a6d4b187ab88d3e3e5c5bc520fcebc42b2960", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "nightly-testing", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 5f11ec894a69ad..bbba35493244d0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "v4.30.0-rc1" +require "leanprover-community" / "batteries" @ git "nightly-testing" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.97" From e51294596c4f249debac2e6c95ed9d7d74368abe Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Apr 2026 02:27:08 +0000 Subject: [PATCH 36/77] fixes --- Mathlib/Algebra/BigOperators/Group/List/Basic.lean | 7 ++----- Mathlib/GroupTheory/FreeGroup/Basic.lean | 6 +++--- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean index 10b0b3e4b5e08d..96546ee4f9951f 100644 --- a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean @@ -244,11 +244,8 @@ lemma prod_map_erase [DecidableEq α] (f : α → M) {a} : @[to_additive] lemma Perm.prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ := h.foldr_op_eq --- In order to make `to_additive` work, this theorem is adjusted to `List.sum_reverse` from core -@[to_additive existing, simp] -lemma prod_reverse [One α] [Mul α] [@Std.Associative α (· * ·)] [@Std.Commutative α (· * ·)] - [@Std.LawfulLeftIdentity α α (· * ·) 1] (l : List α) : prod l.reverse = prod l := - @List.sum_reverse α ⟨1⟩ ⟨(· * ·)⟩ _ _ _ l +set_option linter.existingAttributeWarning false in +attribute [to_additive existing] prod_reverse @[to_additive] lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop : diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean index 5831d64e9de81c..f3473e05b869bc 100644 --- a/Mathlib/GroupTheory/FreeGroup/Basic.lean +++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean @@ -331,14 +331,14 @@ protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ := theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length := h.sublist.length_le - -@[to_additive] +@[to_additive (attr := deprecated "Should not be needed." (since := "2026-04-10"))] theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)}, Step L₁ L₂ → sizeOf L₂ < sizeOf L₁ | _, _, @Step.not _ L1 L2 x b => by induction L1 with | nil => - dsimp + -- This was just `dsimp` prior to https://github.com/leanprover/lean4/pull/13320 + dsimp [sizeOf, _sizeOf_1] lia | cons hd tl ih => dsimp From f55f739a63987e8722eb768ca167937026d38f2a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Apr 2026 03:30:38 +0000 Subject: [PATCH 37/77] fix tests --- MathlibTest/BasicFiles/Init.lean | 2 +- MathlibTest/BasicFiles/Tactic.lean | 2 +- MathlibTest/BasicFiles/TacticBasic.lean | 2 +- MathlibTest/BasicFiles/TacticCommon.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/MathlibTest/BasicFiles/Init.lean b/MathlibTest/BasicFiles/Init.lean index 59ca2efa0b844f..4cbb559c20d688 100644 --- a/MathlibTest/BasicFiles/Init.lean +++ b/MathlibTest/BasicFiles/Init.lean @@ -33,7 +33,7 @@ import Mathlib.Init proof_wanted please_prove_this : True -- Guard against the shake tool modifying our imports -/-- info: [public import Init, import Mathlib.Init] -/ +/-- info: [public import Init, public meta import Init, import Mathlib.Init] -/ #guard_msgs in run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}" diff --git a/MathlibTest/BasicFiles/Tactic.lean b/MathlibTest/BasicFiles/Tactic.lean index 3368b3c7823a2c..3944dcda6da406 100644 --- a/MathlibTest/BasicFiles/Tactic.lean +++ b/MathlibTest/BasicFiles/Tactic.lean @@ -8,6 +8,6 @@ import Mathlib.Tactic #find_syntax "test_find_syntax" approx -- Guard against the shake tool modifying our imports -/-- info: [public import Init, import Mathlib.Tactic] -/ +/-- info: [public import Init, public meta import Init, import Mathlib.Tactic] -/ #guard_msgs in run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}" diff --git a/MathlibTest/BasicFiles/TacticBasic.lean b/MathlibTest/BasicFiles/TacticBasic.lean index f19fa468ff29b1..f1e44b1e8b7eb5 100644 --- a/MathlibTest/BasicFiles/TacticBasic.lean +++ b/MathlibTest/BasicFiles/TacticBasic.lean @@ -5,6 +5,6 @@ import Mathlib.Tactic.Basic /-! Checks that some utilities are available already when importing `Mathlib.Tactic.Basic`. -/ -- Guard against the shake tool modifying our imports -/-- info: [public import Init, import Mathlib.Tactic.Basic] -/ +/-- info: [public import Init, public meta import Init, import Mathlib.Tactic.Basic] -/ #guard_msgs in run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}" diff --git a/MathlibTest/BasicFiles/TacticCommon.lean b/MathlibTest/BasicFiles/TacticCommon.lean index 7c9190b296c047..3ae7c274824d68 100644 --- a/MathlibTest/BasicFiles/TacticCommon.lean +++ b/MathlibTest/BasicFiles/TacticCommon.lean @@ -32,6 +32,6 @@ theorem test_count_heartbeats : True := trivial theorem test_print_sorries : True := sorry -- Guard against the shake tool modifying our imports -/-- info: [public import Init, import Mathlib.Tactic.Common] -/ +/-- info: [public import Init, public meta import Init, import Mathlib.Tactic.Common] -/ #guard_msgs in run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}" From 3f816388b0545a90277feb07b05533b861b6cf98 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Apr 2026 03:39:14 +0000 Subject: [PATCH 38/77] ci: skip inputRev validation on nightly-testing branch Co-Authored-By: Claude Opus 4.6 (1M context) --- .github/workflows/build_template.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml index 4904fb8d237b29..e0afc8a1fb5975 100644 --- a/.github/workflows/build_template.yml +++ b/.github/workflows/build_template.yml @@ -222,7 +222,7 @@ jobs: - name: validate lake-manifest.json inputRevs # Only enforce this on the main mathlib4 repository, not on nightly-testing - if: github.repository == 'leanprover-community/mathlib4' + if: github.repository == 'leanprover-community/mathlib4' && github.ref_name != 'nightly-testing' shell: bash run: | cd pr-branch From d5cca85ca533f1d1f3cf20656fc7ac3aa90960be Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Fri, 10 Apr 2026 09:28:23 +0000 Subject: [PATCH 39/77] chore: bump to nightly-2026-04-10 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index d04b8570d780a2..9187f2ebfc2754 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-09 +leanprover/lean4:nightly-2026-04-10 From aaa0ccc93755fdd58c45d49bdeea9fbf628ae207 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Apr 2026 12:51:02 +0000 Subject: [PATCH 40/77] chore(nolints): add docBlame exceptions for auto-generated `instInhabited.default` Co-Authored-By: Claude Opus 4.6 (1M context) --- scripts/nolints.json | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/nolints.json b/scripts/nolints.json index 60e690f82c2121..28f12584330383 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -224,4 +224,9 @@ ["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"], ["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"], ["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"], - ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"]] + ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"], + ["docBlame", "Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default"], + ["docBlame", "Mathlib.Linter.Flexible.instInhabitedStained.default"], + ["docBlame", "Mathlib.Linter.instInhabitedImportState.default"], + ["docBlame", "Mathlib.Linter.TextBased.instInhabitedStyleError.default"], + ["docBlame", "Mathlib.Linter.instInhabitedFormatError.default"]] From ba9bf0f57e8bc6882141df12167ca3ce52be30c1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Apr 2026 13:05:49 +0000 Subject: [PATCH 41/77] fix(lint-style): filter out duplicate `Init` from `Mathlib.lean` imports `Lean.parseImports'` now emits `Init` more than once for module-system files such as `Mathlib.lean`, but `findImportsFromSource` (in importGraph) only `.erase`s the first occurrence. The remaining `Init` was treated as a module to lint, producing `uncaught exception: no such file or directory ... file: Init.lean` and breaking the `lint-style` CI job on `nightly-testing`. Defensively filter out any remaining `Init` after `findImportsFromSource`. Co-Authored-By: Claude Opus 4.6 (1M context) --- scripts/lint-style.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 05b2e645c49a20..7097007f2de8bf 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -105,7 +105,11 @@ def missingInitImports (opts : LinterOptions) : IO Nat := do -- Find any file in the Mathlib directory which does not contain any Mathlib import. -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date. - let allModuleNames := eraseExplicitImports (← findImportsFromSource "Mathlib.lean") + -- Note: `findImportsFromSource` only erases the *first* occurrence of `Init`. + -- On module-system files (such as `Mathlib.lean`), `Lean.parseImports'` may emit + -- `Init` multiple times, so we filter out any remaining occurrences here. + let allModuleNames := (eraseExplicitImports (← findImportsFromSource "Mathlib.lean")).filter + (· != `Init) let mut modulesWithoutMathlibImports := #[] let mut importsHeaderLinter := #[] for module in allModuleNames do From b6db754b69d7c3e6a3ff338c1b9fabd8a1adea9f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Apr 2026 13:15:45 +0000 Subject: [PATCH 42/77] fix --- Mathlib/Tactic/DefEqAbuse.lean | 4 ++-- Mathlib/Tactic/Linter/DirectoryDependency.lean | 2 +- Mathlib/Tactic/Linter/HashCommandLinter.lean | 4 ++-- Mathlib/Tactic/Linter/MinImports.lean | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Tactic/DefEqAbuse.lean b/Mathlib/Tactic/DefEqAbuse.lean index b72edd96e10676..7475962923f945 100644 --- a/Mathlib/Tactic/DefEqAbuse.lean +++ b/Mathlib/Tactic/DefEqAbuse.lean @@ -299,7 +299,7 @@ Comparison is whitespace-insensitive to handle cases where LHS and RHS are seman but rendered with different line breaks or spacing. TODO: once https://github.com/leanprover/lean4/pull/12698 is available, refactor to use `TraceData.result?` and compare the LHS/RHS `Expr`s structurally instead of string-matching. -/ -private def isIdenticalSidesStr (raw : String) : Bool := +def isIdenticalSidesStr (raw : String) : Bool := if let [lhsRaw, rhs] := raw.splitOn " =?= " then -- Strip the leading status emoji/word (first whitespace-delimited token). let lhs := match lhsRaw.splitOn " " with @@ -315,7 +315,7 @@ private def isIdenticalSidesStr (raw : String) : Bool := Each level adds more detail to pretty-printed expressions. We prefer symmetric options (`pp.universes`, `pp.explicit`) over `pp.analyze`, which is context-dependent and can add annotations to only one side. -/ -private def ppEscalations : List (Options → Options) := +def ppEscalations : List (Options → Options) := [ fun o => o.setBool `pp.universes true , fun o => o.setBool `pp.explicit true ] diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index d048f9b23c198a..24a689902168e5 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -620,7 +620,7 @@ open DirectoryDependency /-- Check if one of the imports `imports` to `mainModule` is forbidden by `forbiddenImportDirs`; if so, return an error describing how the import transitively arises. -/ -private def checkBlocklist (env : Environment) (mainModule : Name) (imports : Array Name) : Option MessageData := Id.run do +def checkBlocklist (env : Environment) (mainModule : Name) (imports : Array Name) : Option MessageData := Id.run do match forbiddenImportDirs.findAny mainModule imports with | some (n₁, n₂) => do if let some imported := n₂.prefixToName imports then diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index 3f2c8f926bef0b..0b9741bd5005ae 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -46,7 +46,7 @@ open Command in /-- Exactly like `withSetOptionIn`, but recursively discards nested uses of `in`. Intended to be used in the `hashCommand` linter, where we want to enter `set_option` `in` commands. -/ -private partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun stx => do +partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun stx => do if stx.getKind == ``Lean.Parser.Command.in then if stx[0].getKind == ``Lean.Parser.Command.set_option then let opts ← Elab.elabSetOption stx[0][1] stx[0][3] @@ -58,7 +58,7 @@ private partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun st cmd stx /-- `allowed_commands` is the `HashSet` of `#`-commands that are allowed in 'Mathlib'. -/ -private abbrev allowed_commands : Std.HashSet String := { "#adaptation_note" } +abbrev allowed_commands : Std.HashSet String := { "#adaptation_note" } /-- Checks that no command beginning with `#` is present in 'Mathlib', except for the ones in `allowed_commands`. diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index ae2a42c439c518..510c707f3e9dbe 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -52,7 +52,7 @@ structure ImportState where /-- `minImportsRef` keeps track of cumulative imports across multiple commands, using `ImportState`. -/ -private initialize minImportsRef : IO.Ref ImportState ← IO.mkRef {} +initialize minImportsRef : IO.Ref ImportState ← IO.mkRef {} /-- `#reset_min_imports` sets to empty the current list of cumulative imports. -/ elab "#reset_min_imports" : command => minImportsRef.set {} From f053cf0373d5987130c5aa0669d505209827612c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Apr 2026 16:11:39 +0000 Subject: [PATCH 43/77] fix plausible --- lake-manifest.json | 20 ++++++++++---------- lakefile.lean | 2 +- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index d47be9b382b89e..fdf39b00ac9c1f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,14 +1,14 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/plausible", + [{"url": "https://github.com/Kha/plausible", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "4d955ffd04d5f6d1143c5bf8fffab59ea7d84595", + "scope": "", + "rev": "1e454fed5528d2df0f45708f6b9e8e519c47fc5a", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "push-nuzuuroszpvz", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4270b99dc7c5e90d5ee5c6cb2dd91aaba5b19557", + "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ac0e066410c02c7f755c865c2a4770855d47291", + "rev": "ad416ddf6cc9d5b1c00eaf04a48e703538132760", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0b2df33836dabcfbb05acaf73179ca8bb21c34cf", + "rev": "bee778191c7fbea31864ecfe1809b8837626aba0", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "257610310763a697d819165a58f209a63a512929", + "rev": "09de4da19089efce3746d2b69930387b4709f110", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13132", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "33583e6fb5096defc38f0c7f67d1c4a3825aee1f", + "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc7", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "mathlib", diff --git a/lakefile.lean b/lakefile.lean index a52a5fdfd39591..d5c82b86b819d4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,7 +16,7 @@ require "leanprover-community" / "proofwidgets" @ git "v0.0.92-pre1" -- ProofWid If this does not work, report your issue on the Lean Zulip." require "leanprover-community" / "importGraph" @ git "main" require "leanprover-community" / "LeanSearchClient" @ git "main" -require "leanprover-community" / "plausible" @ git "main" +require plausible from git "https://github.com/Kha/plausible" @ "push-nuzuuroszpvz" /-! From a1c9945976087d1e6b8226b856c5c19ca2dda1ab Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 11 Apr 2026 01:05:24 +0000 Subject: [PATCH 44/77] chore: update importGraph, remove duplicate Init workaround MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Updates importGraph to pick up leanprover-community/import-graph#115, which fixes `findImportsFromSource` to filter (not just erase) `Init`. This removes the need for the defensive `.filter (· != `Init)` we added to `lint-style.lean`. Co-Authored-By: Claude Opus 4.6 (1M context) --- lake-manifest.json | 6 +++--- scripts/lint-style.lean | 6 +----- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7071f31f8baa9e..b3d3a8b9363482 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a3b459a8312125758e51c354b93d54ba620efda6", + "rev": "2541d6b9e923b0b2f867d7b037ac344551cc7feb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7", + "rev": "4411c5f89c797401c609b3a946c8874569e69731", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ac74d33e9166b34a985f7c774a9e7f4b1c1adc35", + "rev": "896fee4b88a27faa234591ab515a6f9f70f9a096", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 7097007f2de8bf..05b2e645c49a20 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -105,11 +105,7 @@ def missingInitImports (opts : LinterOptions) : IO Nat := do -- Find any file in the Mathlib directory which does not contain any Mathlib import. -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date. - -- Note: `findImportsFromSource` only erases the *first* occurrence of `Init`. - -- On module-system files (such as `Mathlib.lean`), `Lean.parseImports'` may emit - -- `Init` multiple times, so we filter out any remaining occurrences here. - let allModuleNames := (eraseExplicitImports (← findImportsFromSource "Mathlib.lean")).filter - (· != `Init) + let allModuleNames := eraseExplicitImports (← findImportsFromSource "Mathlib.lean") let mut modulesWithoutMathlibImports := #[] let mut importsHeaderLinter := #[] for module in allModuleNames do From 0ab07d5e95e2928ad3810de7d682c51a68cac49d Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Sat, 11 Apr 2026 14:59:26 +0000 Subject: [PATCH 45/77] chore: bump to nightly-2026-04-11 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 9187f2ebfc2754..bca52a66f4273a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-10 +leanprover/lean4:nightly-2026-04-11 From 8da25c31bbe645ed439257ff710a4c1df21f0172 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 11 Apr 2026 23:52:27 +0000 Subject: [PATCH 46/77] silence linter --- Mathlib/Combinatorics/Matroid/Init.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Init.lean | 2 +- Mathlib/Data/Finset/Attr.lean | 2 +- Mathlib/Data/Sym/Sym2/Init.lean | 2 +- Mathlib/Tactic/ArithMult/Init.lean | 2 +- Mathlib/Tactic/Bound/Init.lean | 2 +- Mathlib/Tactic/Continuity/Init.lean | 2 +- Mathlib/Tactic/Finiteness/Attr.lean | 2 +- Mathlib/Tactic/FunProp/Attr.lean | 4 +++- Mathlib/Tactic/Measurability/Init.lean | 2 +- Mathlib/Topology/Sheaves/Init.lean | 2 +- 11 files changed, 13 insertions(+), 11 deletions(-) diff --git a/Mathlib/Combinatorics/Matroid/Init.lean b/Mathlib/Combinatorics/Matroid/Init.lean index 6e434c01bdf627..ea8bd6b7ef7fdb 100644 --- a/Mathlib/Combinatorics/Matroid/Init.lean +++ b/Mathlib/Combinatorics/Matroid/Init.lean @@ -16,6 +16,6 @@ This module defines the `Matroid` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public section +set_option linter.privateModule false declare_aesop_rule_sets [Matroid] diff --git a/Mathlib/Combinatorics/SimpleGraph/Init.lean b/Mathlib/Combinatorics/SimpleGraph/Init.lean index e33f62ae3c0e25..036d3d9068a3ea 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Init.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Init.lean @@ -16,6 +16,6 @@ This module defines the `SimpleGraph` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public section +set_option linter.privateModule false declare_aesop_rule_sets [SimpleGraph] diff --git a/Mathlib/Data/Finset/Attr.lean b/Mathlib/Data/Finset/Attr.lean index 19a757ed46f9aa..73ea5e2f67435b 100644 --- a/Mathlib/Data/Finset/Attr.lean +++ b/Mathlib/Data/Finset/Attr.lean @@ -14,7 +14,7 @@ public import Aesop.Frontend This file defines `finsetNonempty`, an aesop rule set to prove that a given finset is nonempty. -/ -public section +set_option linter.privateModule false -- `finsetNonempty` rules try to prove that a given finset is nonempty, -- for use in positivity extensions. diff --git a/Mathlib/Data/Sym/Sym2/Init.lean b/Mathlib/Data/Sym/Sym2/Init.lean index cda8468ef86fa9..c51268af88812f 100644 --- a/Mathlib/Data/Sym/Sym2/Init.lean +++ b/Mathlib/Data/Sym/Sym2/Init.lean @@ -16,6 +16,6 @@ visible once the file in which they're declared is imported, so we must put this declaration into its own file. -/ -public section +set_option linter.privateModule false declare_aesop_rule_sets [Sym2] diff --git a/Mathlib/Tactic/ArithMult/Init.lean b/Mathlib/Tactic/ArithMult/Init.lean index 4c95026124c1a6..f65598b911fe16 100644 --- a/Mathlib/Tactic/ArithMult/Init.lean +++ b/Mathlib/Tactic/ArithMult/Init.lean @@ -16,6 +16,6 @@ This module defines the `IsMultiplicative` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section +set_option linter.privateModule false declare_aesop_rule_sets [IsMultiplicative] diff --git a/Mathlib/Tactic/Bound/Init.lean b/Mathlib/Tactic/Bound/Init.lean index 8168cf288aefd4..a41685bdb3b91e 100644 --- a/Mathlib/Tactic/Bound/Init.lean +++ b/Mathlib/Tactic/Bound/Init.lean @@ -16,6 +16,6 @@ This module defines the `Bound` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section +set_option linter.privateModule false declare_aesop_rule_sets [Bound] diff --git a/Mathlib/Tactic/Continuity/Init.lean b/Mathlib/Tactic/Continuity/Init.lean index e988564a6b947d..05428ea6dd0d9c 100644 --- a/Mathlib/Tactic/Continuity/Init.lean +++ b/Mathlib/Tactic/Continuity/Init.lean @@ -16,6 +16,6 @@ This module defines the `Continuous` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section +set_option linter.privateModule false declare_aesop_rule_sets [Continuous] diff --git a/Mathlib/Tactic/Finiteness/Attr.lean b/Mathlib/Tactic/Finiteness/Attr.lean index bb64d9e46af3de..e6946c319bd774 100644 --- a/Mathlib/Tactic/Finiteness/Attr.lean +++ b/Mathlib/Tactic/Finiteness/Attr.lean @@ -10,6 +10,6 @@ public import Aesop.Frontend /-! # Finiteness tactic attribute -/ -public meta section +set_option linter.privateModule false declare_aesop_rule_sets [finiteness] diff --git a/Mathlib/Tactic/FunProp/Attr.lean b/Mathlib/Tactic/FunProp/Attr.lean index e0e8b89ad02e2f..10550960a98fc3 100644 --- a/Mathlib/Tactic/FunProp/Attr.lean +++ b/Mathlib/Tactic/FunProp/Attr.lean @@ -12,7 +12,9 @@ public import Mathlib.Tactic.FunProp.Theorems ## `funProp` attribute -/ -public meta section +set_option linter.privateModule false + +meta section namespace Mathlib open Lean Meta diff --git a/Mathlib/Tactic/Measurability/Init.lean b/Mathlib/Tactic/Measurability/Init.lean index 85e8ae3add56fb..16f02034afa7ce 100644 --- a/Mathlib/Tactic/Measurability/Init.lean +++ b/Mathlib/Tactic/Measurability/Init.lean @@ -16,6 +16,6 @@ This module defines the `Measurable` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section +set_option linter.privateModule false declare_aesop_rule_sets [Measurable] diff --git a/Mathlib/Topology/Sheaves/Init.lean b/Mathlib/Topology/Sheaves/Init.lean index 053c3cdee10982..2556c0ac7d7595 100644 --- a/Mathlib/Topology/Sheaves/Init.lean +++ b/Mathlib/Topology/Sheaves/Init.lean @@ -16,7 +16,7 @@ visible once the file in which they're declared is imported, so we must put this declaration into its own file. -/ -public section +set_option linter.privateModule false /- to prove subset relations -/ declare_aesop_rule_sets [Restrict] From d2d45e83089fcb3e28184674ef50eb8de150c20d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 12 Apr 2026 00:59:17 +0000 Subject: [PATCH 47/77] broken test: still broken, but doesn't stop the build. --- MathlibTest/PrivateModuleLinter/initialize.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MathlibTest/PrivateModuleLinter/initialize.lean b/MathlibTest/PrivateModuleLinter/initialize.lean index 7d5b5a0db2e050..4d7e3a2a7e339e 100644 --- a/MathlibTest/PrivateModuleLinter/initialize.lean +++ b/MathlibTest/PrivateModuleLinter/initialize.lean @@ -2,7 +2,7 @@ module import Mathlib.Tactic.Linter.PrivateModule -set_option linter.privateModule true +set_option linter.privateModule false -- Changed in nightly-testing, as this test no longer works. open Lean From eb7a77483db8367698858255fafa3b594faecd86 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sat, 11 Apr 2026 23:44:06 -0400 Subject: [PATCH 48/77] fix: exempt files registering initializers from the `privateModule` linter --- Mathlib/Tactic/Linter/PrivateModule.lean | 33 ++++++++++++++---------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean index 08905121646445..bf5a2aa6a32502 100644 --- a/Mathlib/Tactic/Linter/PrivateModule.lean +++ b/Mathlib/Tactic/Linter/PrivateModule.lean @@ -26,6 +26,9 @@ the file. Note that private declarations from the current module are exactly those which satisfy `isPrivateName`, whether private due to an explicit `private` or due to not being made `public`. +Since initializers have downstream effects regardless of whether they're `private` or `public`, any +module which registers an initializer is considered non-private. + We also do not count declarations which satisfy `isReservedName` as public declarations *from the current module*. While they might indeed be public, the declarations associated with reserved names are generated automatically and lazily, sometimes in downstream modules from the one in which the @@ -46,8 +49,7 @@ See also the type `Lean.ReservedNameAction`, invocations of `registerReservedNam Note that metaprograms should not add public declarations when run in private scopes. Doing so would likely be a bug in the metaprogram. As such, we do not perform further checks for automatically -generated declarations such as those detected by `isAutoDecl` or `isInternalDetail`, which would -wrongly exclude e.g. public declarations generated by `initialize`. +generated declarations such as those detected by `isAutoDecl` or `isInternalDetail`. -/ meta section @@ -75,19 +77,22 @@ def privateModule : Linter where run stx := do if stx.isOfKind ``Parser.Command.eoi then unless getLinterValue linter.privateModule (← getLinterOptions) do return - if (← getEnv).header.isModule then + if (← getEnv).header.isModule + -- If there are new initializers, this module has a downstream effect and is not private. + && (regularInitAttr.ext.getState (← getEnv)).1.isEmpty -- Don't lint an imports-only module: - if !(← getEnv).constants.map₂.isEmpty then - -- Exit if any declaration from the current module is public: - for (decl, _) in (← getEnv).constants.map₂ do - -- Ignore both private and reserved names; see implementation notes - if !isPrivateName decl && !isReservedName (← getEnv) decl then return - -- Lint if all names are private: - let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) "" - logLint linter.privateModule topOfFileRef - "The current module only contains private declarations.\n\n\ - Consider adding `@[expose] public section` at the beginning of the module, \ - or selectively marking declarations as `public`." + && !(← getEnv).constants.map₂.isEmpty + then + -- Exit if any declaration from the current module is public: + for (decl, _) in (← getEnv).constants.map₂ do + -- Ignore both private and reserved names; see implementation notes + if !isPrivateName decl && !isReservedName (← getEnv) decl then return + -- Lint if all names are private: + let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) "" + logLint linter.privateModule topOfFileRef + "The current module only contains private declarations.\n\n\ + Consider adding `@[expose] public section` at the beginning of the module, \ + or selectively marking declarations as `public`." initialize addLinter privateModule From 853d41e08f58f1553cfd58fd1d7f66abd438a815 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sat, 11 Apr 2026 23:45:52 -0400 Subject: [PATCH 49/77] Revert "silence linter" This reverts commit 8da25c31bbe645ed439257ff710a4c1df21f0172. --- Mathlib/Combinatorics/Matroid/Init.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Init.lean | 2 +- Mathlib/Data/Finset/Attr.lean | 2 +- Mathlib/Data/Sym/Sym2/Init.lean | 2 +- Mathlib/Tactic/ArithMult/Init.lean | 2 +- Mathlib/Tactic/Bound/Init.lean | 2 +- Mathlib/Tactic/Continuity/Init.lean | 2 +- Mathlib/Tactic/Finiteness/Attr.lean | 2 +- Mathlib/Tactic/FunProp/Attr.lean | 4 +--- Mathlib/Tactic/Measurability/Init.lean | 2 +- Mathlib/Topology/Sheaves/Init.lean | 2 +- 11 files changed, 11 insertions(+), 13 deletions(-) diff --git a/Mathlib/Combinatorics/Matroid/Init.lean b/Mathlib/Combinatorics/Matroid/Init.lean index ea8bd6b7ef7fdb..6e434c01bdf627 100644 --- a/Mathlib/Combinatorics/Matroid/Init.lean +++ b/Mathlib/Combinatorics/Matroid/Init.lean @@ -16,6 +16,6 @@ This module defines the `Matroid` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public section declare_aesop_rule_sets [Matroid] diff --git a/Mathlib/Combinatorics/SimpleGraph/Init.lean b/Mathlib/Combinatorics/SimpleGraph/Init.lean index 036d3d9068a3ea..e33f62ae3c0e25 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Init.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Init.lean @@ -16,6 +16,6 @@ This module defines the `SimpleGraph` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public section declare_aesop_rule_sets [SimpleGraph] diff --git a/Mathlib/Data/Finset/Attr.lean b/Mathlib/Data/Finset/Attr.lean index 73ea5e2f67435b..19a757ed46f9aa 100644 --- a/Mathlib/Data/Finset/Attr.lean +++ b/Mathlib/Data/Finset/Attr.lean @@ -14,7 +14,7 @@ public import Aesop.Frontend This file defines `finsetNonempty`, an aesop rule set to prove that a given finset is nonempty. -/ -set_option linter.privateModule false +public section -- `finsetNonempty` rules try to prove that a given finset is nonempty, -- for use in positivity extensions. diff --git a/Mathlib/Data/Sym/Sym2/Init.lean b/Mathlib/Data/Sym/Sym2/Init.lean index c51268af88812f..cda8468ef86fa9 100644 --- a/Mathlib/Data/Sym/Sym2/Init.lean +++ b/Mathlib/Data/Sym/Sym2/Init.lean @@ -16,6 +16,6 @@ visible once the file in which they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public section declare_aesop_rule_sets [Sym2] diff --git a/Mathlib/Tactic/ArithMult/Init.lean b/Mathlib/Tactic/ArithMult/Init.lean index f65598b911fe16..4c95026124c1a6 100644 --- a/Mathlib/Tactic/ArithMult/Init.lean +++ b/Mathlib/Tactic/ArithMult/Init.lean @@ -16,6 +16,6 @@ This module defines the `IsMultiplicative` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public meta section declare_aesop_rule_sets [IsMultiplicative] diff --git a/Mathlib/Tactic/Bound/Init.lean b/Mathlib/Tactic/Bound/Init.lean index a41685bdb3b91e..8168cf288aefd4 100644 --- a/Mathlib/Tactic/Bound/Init.lean +++ b/Mathlib/Tactic/Bound/Init.lean @@ -16,6 +16,6 @@ This module defines the `Bound` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public meta section declare_aesop_rule_sets [Bound] diff --git a/Mathlib/Tactic/Continuity/Init.lean b/Mathlib/Tactic/Continuity/Init.lean index 05428ea6dd0d9c..e988564a6b947d 100644 --- a/Mathlib/Tactic/Continuity/Init.lean +++ b/Mathlib/Tactic/Continuity/Init.lean @@ -16,6 +16,6 @@ This module defines the `Continuous` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public meta section declare_aesop_rule_sets [Continuous] diff --git a/Mathlib/Tactic/Finiteness/Attr.lean b/Mathlib/Tactic/Finiteness/Attr.lean index e6946c319bd774..bb64d9e46af3de 100644 --- a/Mathlib/Tactic/Finiteness/Attr.lean +++ b/Mathlib/Tactic/Finiteness/Attr.lean @@ -10,6 +10,6 @@ public import Aesop.Frontend /-! # Finiteness tactic attribute -/ -set_option linter.privateModule false +public meta section declare_aesop_rule_sets [finiteness] diff --git a/Mathlib/Tactic/FunProp/Attr.lean b/Mathlib/Tactic/FunProp/Attr.lean index 10550960a98fc3..e0e8b89ad02e2f 100644 --- a/Mathlib/Tactic/FunProp/Attr.lean +++ b/Mathlib/Tactic/FunProp/Attr.lean @@ -12,9 +12,7 @@ public import Mathlib.Tactic.FunProp.Theorems ## `funProp` attribute -/ -set_option linter.privateModule false - -meta section +public meta section namespace Mathlib open Lean Meta diff --git a/Mathlib/Tactic/Measurability/Init.lean b/Mathlib/Tactic/Measurability/Init.lean index 16f02034afa7ce..85e8ae3add56fb 100644 --- a/Mathlib/Tactic/Measurability/Init.lean +++ b/Mathlib/Tactic/Measurability/Init.lean @@ -16,6 +16,6 @@ This module defines the `Measurable` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public meta section declare_aesop_rule_sets [Measurable] diff --git a/Mathlib/Topology/Sheaves/Init.lean b/Mathlib/Topology/Sheaves/Init.lean index 2556c0ac7d7595..053c3cdee10982 100644 --- a/Mathlib/Topology/Sheaves/Init.lean +++ b/Mathlib/Topology/Sheaves/Init.lean @@ -16,7 +16,7 @@ visible once the file in which they're declared is imported, so we must put this declaration into its own file. -/ -set_option linter.privateModule false +public section /- to prove subset relations -/ declare_aesop_rule_sets [Restrict] From 7a5e5b4706f978e7d67bc1e22d7941809deed670 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sat, 11 Apr 2026 23:57:50 -0400 Subject: [PATCH 50/77] chore: remove unused sections in front of lone `declare_aesop_rule_sets` --- Mathlib/Combinatorics/Matroid/Init.lean | 2 -- Mathlib/Combinatorics/SimpleGraph/Init.lean | 2 -- Mathlib/Data/Finset/Attr.lean | 2 -- Mathlib/Data/Sym/Sym2/Init.lean | 2 -- Mathlib/Tactic/ArithMult/Init.lean | 2 -- Mathlib/Tactic/Bound/Init.lean | 2 -- Mathlib/Tactic/Continuity/Init.lean | 2 -- Mathlib/Tactic/Finiteness/Attr.lean | 2 -- Mathlib/Tactic/Measurability/Init.lean | 2 -- Mathlib/Topology/Sheaves/Init.lean | 2 -- 10 files changed, 20 deletions(-) diff --git a/Mathlib/Combinatorics/Matroid/Init.lean b/Mathlib/Combinatorics/Matroid/Init.lean index 6e434c01bdf627..bf806f06d08923 100644 --- a/Mathlib/Combinatorics/Matroid/Init.lean +++ b/Mathlib/Combinatorics/Matroid/Init.lean @@ -16,6 +16,4 @@ This module defines the `Matroid` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public section - declare_aesop_rule_sets [Matroid] diff --git a/Mathlib/Combinatorics/SimpleGraph/Init.lean b/Mathlib/Combinatorics/SimpleGraph/Init.lean index e33f62ae3c0e25..0928e07666be5f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Init.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Init.lean @@ -16,6 +16,4 @@ This module defines the `SimpleGraph` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public section - declare_aesop_rule_sets [SimpleGraph] diff --git a/Mathlib/Data/Finset/Attr.lean b/Mathlib/Data/Finset/Attr.lean index 19a757ed46f9aa..a8894132142c32 100644 --- a/Mathlib/Data/Finset/Attr.lean +++ b/Mathlib/Data/Finset/Attr.lean @@ -14,8 +14,6 @@ public import Aesop.Frontend This file defines `finsetNonempty`, an aesop rule set to prove that a given finset is nonempty. -/ -public section - -- `finsetNonempty` rules try to prove that a given finset is nonempty, -- for use in positivity extensions. declare_aesop_rule_sets [finsetNonempty] (default := true) diff --git a/Mathlib/Data/Sym/Sym2/Init.lean b/Mathlib/Data/Sym/Sym2/Init.lean index cda8468ef86fa9..69faa4d163130c 100644 --- a/Mathlib/Data/Sym/Sym2/Init.lean +++ b/Mathlib/Data/Sym/Sym2/Init.lean @@ -16,6 +16,4 @@ visible once the file in which they're declared is imported, so we must put this declaration into its own file. -/ -public section - declare_aesop_rule_sets [Sym2] diff --git a/Mathlib/Tactic/ArithMult/Init.lean b/Mathlib/Tactic/ArithMult/Init.lean index 4c95026124c1a6..4afdad3dd49e0f 100644 --- a/Mathlib/Tactic/ArithMult/Init.lean +++ b/Mathlib/Tactic/ArithMult/Init.lean @@ -16,6 +16,4 @@ This module defines the `IsMultiplicative` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section - declare_aesop_rule_sets [IsMultiplicative] diff --git a/Mathlib/Tactic/Bound/Init.lean b/Mathlib/Tactic/Bound/Init.lean index 8168cf288aefd4..f2a48a6687e866 100644 --- a/Mathlib/Tactic/Bound/Init.lean +++ b/Mathlib/Tactic/Bound/Init.lean @@ -16,6 +16,4 @@ This module defines the `Bound` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section - declare_aesop_rule_sets [Bound] diff --git a/Mathlib/Tactic/Continuity/Init.lean b/Mathlib/Tactic/Continuity/Init.lean index e988564a6b947d..19e4f9da717012 100644 --- a/Mathlib/Tactic/Continuity/Init.lean +++ b/Mathlib/Tactic/Continuity/Init.lean @@ -16,6 +16,4 @@ This module defines the `Continuous` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section - declare_aesop_rule_sets [Continuous] diff --git a/Mathlib/Tactic/Finiteness/Attr.lean b/Mathlib/Tactic/Finiteness/Attr.lean index bb64d9e46af3de..226794663ee9b0 100644 --- a/Mathlib/Tactic/Finiteness/Attr.lean +++ b/Mathlib/Tactic/Finiteness/Attr.lean @@ -10,6 +10,4 @@ public import Aesop.Frontend /-! # Finiteness tactic attribute -/ -public meta section - declare_aesop_rule_sets [finiteness] diff --git a/Mathlib/Tactic/Measurability/Init.lean b/Mathlib/Tactic/Measurability/Init.lean index 85e8ae3add56fb..20debd09a5bf8b 100644 --- a/Mathlib/Tactic/Measurability/Init.lean +++ b/Mathlib/Tactic/Measurability/Init.lean @@ -16,6 +16,4 @@ This module defines the `Measurable` Aesop rule set which is used by the they're declared is imported, so we must put this declaration into its own file. -/ -public meta section - declare_aesop_rule_sets [Measurable] diff --git a/Mathlib/Topology/Sheaves/Init.lean b/Mathlib/Topology/Sheaves/Init.lean index 053c3cdee10982..f5fc267eee2827 100644 --- a/Mathlib/Topology/Sheaves/Init.lean +++ b/Mathlib/Topology/Sheaves/Init.lean @@ -16,7 +16,5 @@ visible once the file in which they're declared is imported, so we must put this declaration into its own file. -/ -public section - /- to prove subset relations -/ declare_aesop_rule_sets [Restrict] From 8568f337c9d994d0b5080c81dba80bde96b17773 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sun, 12 Apr 2026 00:00:57 -0400 Subject: [PATCH 51/77] chore: restore `initialize` test for `privateModule` linter with correct wording --- MathlibTest/PrivateModuleLinter/initialize.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/MathlibTest/PrivateModuleLinter/initialize.lean b/MathlibTest/PrivateModuleLinter/initialize.lean index 4d7e3a2a7e339e..0cc6d129a209b2 100644 --- a/MathlibTest/PrivateModuleLinter/initialize.lean +++ b/MathlibTest/PrivateModuleLinter/initialize.lean @@ -2,11 +2,9 @@ module import Mathlib.Tactic.Linter.PrivateModule -set_option linter.privateModule false -- Changed in nightly-testing, as this test no longer works. - open Lean --- Should not fire, since `initialize` creates a genuinely public declaration. +-- Should not fire, since `initialize` has effects downstream despite creating a private decl here. initialize pure () /- Check that we have indeed created a declaration, and aren't not linting just due to being an From d49f1edb8c3c52b4d6b64537efdddd7f320cec12 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sun, 12 Apr 2026 00:02:11 -0400 Subject: [PATCH 52/77] chore: restore `privateModule` `initialize` test with linter turned on --- MathlibTest/PrivateModuleLinter/initialize.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/MathlibTest/PrivateModuleLinter/initialize.lean b/MathlibTest/PrivateModuleLinter/initialize.lean index 0cc6d129a209b2..2b8a212c1dd662 100644 --- a/MathlibTest/PrivateModuleLinter/initialize.lean +++ b/MathlibTest/PrivateModuleLinter/initialize.lean @@ -4,6 +4,8 @@ import Mathlib.Tactic.Linter.PrivateModule open Lean +set_option linter.privateModule true + -- Should not fire, since `initialize` has effects downstream despite creating a private decl here. initialize pure () From 365191c6c9c65a53619deda0d752e5d47de563ef Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 12 Apr 2026 08:42:35 +0000 Subject: [PATCH 53/77] fixes --- scripts/create_deprecated_modules.lean | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/scripts/create_deprecated_modules.lean b/scripts/create_deprecated_modules.lean index 9017f4fee82a7f..d17459a8128f45 100644 --- a/scripts/create_deprecated_modules.lean +++ b/scripts/create_deprecated_modules.lean @@ -5,6 +5,7 @@ Authors: Damiano Testa -/ --import Mathlib.Init +import Std.Time.Format import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -- a comment here to test `keepTrailing @@ -49,8 +50,12 @@ It returns just the imports of `fileContent`, including trailing comments if `ke -/ def getHeader (fname fileContent : String) (keepTrailing : Bool) : IO String := do let (stx, _) ← Parser.parseHeader (Parser.mkInputContext fileContent fname) - let stx := if keepTrailing then stx.raw else stx.raw.unsetTrailing - let some substring := stx.getSubstring? | throw <| .userError "No substring: we have a problem!" + let imports := stx.raw.getArg 2 -- extract just the imports list + let imports := if keepTrailing then imports else imports.unsetTrailing + -- Use `withLeading := false` to exclude leading comments (e.g. copyright header) that the + -- parser now attaches to the first token (see leanprover/lean4#12662). + let some substring := imports.getSubstring? (withLeading := false) | + throw <| .userError "No substring: we have a problem!" return substring.toString /-- @@ -374,7 +379,8 @@ the deprecations later on. -- #find_deleted_files 0 /-- -info: import Std.Time.Zoned +info: import Std.Time.Format +import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -/ #guard_msgs in @@ -384,7 +390,8 @@ run_cmd logInfo head /-- -info: import Std.Time.Zoned +info: import Std.Time.Format +import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -- a comment here to test `keepTrailing -/ From 7913a6962ac866777c53bbd9586bada367e78e09 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 13 Apr 2026 08:20:09 +1000 Subject: [PATCH 54/77] fix from nightly-testing --- scripts/create_deprecated_modules.lean | 20 +++----------------- 1 file changed, 3 insertions(+), 17 deletions(-) diff --git a/scripts/create_deprecated_modules.lean b/scripts/create_deprecated_modules.lean index 3b0d79fd3b8ebf..17dff24f395335 100644 --- a/scripts/create_deprecated_modules.lean +++ b/scripts/create_deprecated_modules.lean @@ -371,17 +371,10 @@ replaced by the suggestion, which means that you can click on multiple suggestio the deprecations later on. -/ --- #find_deleted_files 0 +#find_deleted_files 0 /-- -info: /- -Copyright (c) 2025 Damiano Testa. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Damiano Testa --/ - ---import Mathlib.Init -import Std.Time.Zoned +info: import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -/ #guard_msgs in @@ -391,14 +384,7 @@ run_cmd logInfo head /-- -info: /- -Copyright (c) 2025 Damiano Testa. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Damiano Testa --/ - ---import Mathlib.Init -import Std.Time.Zoned +info: import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -- a comment here to test `keepTrailing -/ From af85844a19259e2b76e10ac00aa22a0348c31a17 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 13 Apr 2026 08:24:45 +1000 Subject: [PATCH 55/77] importGraph has been fixed --- lake-manifest.json | 2 +- scripts/lint-style.lean | 6 +----- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 918a1a5ac43321..b3d3a8b9363482 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7", + "rev": "4411c5f89c797401c609b3a946c8874569e69731", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 7097007f2de8bf..05b2e645c49a20 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -105,11 +105,7 @@ def missingInitImports (opts : LinterOptions) : IO Nat := do -- Find any file in the Mathlib directory which does not contain any Mathlib import. -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date. - -- Note: `findImportsFromSource` only erases the *first* occurrence of `Init`. - -- On module-system files (such as `Mathlib.lean`), `Lean.parseImports'` may emit - -- `Init` multiple times, so we filter out any remaining occurrences here. - let allModuleNames := (eraseExplicitImports (← findImportsFromSource "Mathlib.lean")).filter - (· != `Init) + let allModuleNames := eraseExplicitImports (← findImportsFromSource "Mathlib.lean") let mut modulesWithoutMathlibImports := #[] let mut importsHeaderLinter := #[] for module in allModuleNames do From 0b824b59da6ab7e9b1d598416f3c07cb8137e3ef Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Mon, 13 Apr 2026 09:33:27 +0000 Subject: [PATCH 56/77] chore: bump to nightly-2026-04-13 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index bca52a66f4273a..eb7023afec000d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-11 +leanprover/lean4:nightly-2026-04-13 From 7fccdee8587247143421f4aea5bc60035a851340 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 13 Apr 2026 11:15:00 +0000 Subject: [PATCH 57/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13325 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a1b37fd9243976..a4a8a9d9a0de9f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5a746178d12920eacc8a331c80317e7ffbbee780", + "rev": "09f3c93cdbb79f431c5267e8373be9f331341f76", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-13325", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index bbba35493244d0..eb8c895fb557b3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-13325" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.97" diff --git a/lean-toolchain b/lean-toolchain index eb7023afec000d..00bd7e748c28d0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-13 +leanprover/lean4-pr-releases:pr-release-13325-8c01b1b From 02083f3e83ec8cf926ae79f9d85b5eed8f2ab1e0 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 13 Apr 2026 11:57:04 +0000 Subject: [PATCH 58/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13325 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a4a8a9d9a0de9f..f1adde96a1c498 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "09f3c93cdbb79f431c5267e8373be9f331341f76", + "rev": "6bd6d39000c7c175ed1cc88f00ef682d31be8b6a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13325", diff --git a/lean-toolchain b/lean-toolchain index 00bd7e748c28d0..4838ce217e5977 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13325-8c01b1b +leanprover/lean4-pr-releases:pr-release-13325-89c4bb1 From 19b8510ad7a020acb1fa66b3e8882cf34dfb829c Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 13 Apr 2026 12:58:35 +0000 Subject: [PATCH 59/77] chore: silence simp `varHead` and `varOther` warnings --- Mathlib/Algebra/CharP/Two.lean | 1 + Mathlib/Algebra/Order/Floor/Div.lean | 2 ++ Mathlib/CategoryTheory/Sites/Precoverage.lean | 2 ++ Mathlib/Logic/Embedding/Set.lean | 1 + 4 files changed, 6 insertions(+) diff --git a/Mathlib/Algebra/CharP/Two.lean b/Mathlib/Algebra/CharP/Two.lean index 19803221084e16..225971bc7c3983 100644 --- a/Mathlib/Algebra/CharP/Two.lean +++ b/Mathlib/Algebra/CharP/Two.lean @@ -64,6 +64,7 @@ theorem natCast_cases (n : ℕ) : (n : R) = 0 ∨ (n : R) = 1 := theorem natCast_eq_mod (n : ℕ) : (n : R) = (n % 2 : ℕ) := by simp [natCast_eq_ite, Nat.even_iff] +set_option warning.simp.varHead false in @[scoped simp] theorem ofNat_eq_mod (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) = (ofNat(n) % 2 : ℕ) := natCast_eq_mod n diff --git a/Mathlib/Algebra/Order/Floor/Div.lean b/Mathlib/Algebra/Order/Floor/Div.lean index 25998333bb4b4a..523dd9abe57ed2 100644 --- a/Mathlib/Algebra/Order/Floor/Div.lean +++ b/Mathlib/Algebra/Order/Floor/Div.lean @@ -248,6 +248,7 @@ noncomputable instance instFloorDiv : FloorDiv α (ι →₀ β) where zero_floorDiv a := by ext; exact zero_floorDiv _ lemma floorDiv_def (f : ι →₀ β) (a : α) : f ⌊/⌋ a = f.mapRange (· ⌊/⌋ a) (zero_floorDiv _) := rfl +set_option warning.simp.otherHead false in @[norm_cast] lemma coe_floorDiv (f : ι →₀ β) (a : α) : f ⌊/⌋ a = fun i ↦ f i ⌊/⌋ a := rfl @[simp] lemma floorDiv_apply (f : ι →₀ β) (a : α) (i : ι) : (f ⌊/⌋ a) i = f i ⌊/⌋ a := rfl @@ -267,6 +268,7 @@ noncomputable instance instCeilDiv : CeilDiv α (ι →₀ β) where zero_ceilDiv a := by ext; exact zero_ceilDiv _ lemma ceilDiv_def (f : ι →₀ β) (a : α) : f ⌈/⌉ a = f.mapRange (· ⌈/⌉ a) (zero_ceilDiv _) := rfl +set_option warning.simp.otherHead false in @[norm_cast] lemma coe_ceilDiv_def (f : ι →₀ β) (a : α) : f ⌈/⌉ a = fun i ↦ f i ⌈/⌉ a := rfl @[simp] lemma ceilDiv_apply (f : ι →₀ β) (a : α) (i : ι) : (f ⌈/⌉ a) i = f i ⌈/⌉ a := rfl diff --git a/Mathlib/CategoryTheory/Sites/Precoverage.lean b/Mathlib/CategoryTheory/Sites/Precoverage.lean index c0a15ddcefc338..2292a10b1b816d 100644 --- a/Mathlib/CategoryTheory/Sites/Precoverage.lean +++ b/Mathlib/CategoryTheory/Sites/Precoverage.lean @@ -126,6 +126,7 @@ alias mem_coverings_of_isIso := HasIsos.mem_coverings_of_isIso alias sup_mem_coverings := IsStableUnderSup.sup_mem_coverings alias hasPullbacks_of_mem := HasPullbacks.hasPullbacks_of_mem +set_option warning.simp.varHead false in attribute [local simp] Presieve.ofArrows.obj_idx Presieve.ofArrows.hom_idx in lemma mem_coverings_of_isPullback {J : Precoverage C} [IsStableUnderBaseChange J] {ι : Type w} {S : C} {X : ι → C} @@ -146,6 +147,7 @@ lemma mem_coverings_of_isPullback {J : Precoverage C} [IsStableUnderBaseChange J refine le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_ exact .mk' (Sum.inl ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch) +set_option warning.simp.varHead false in attribute [local simp] Presieve.ofArrows.obj_idx Presieve.ofArrows.hom_idx in lemma comp_mem_coverings {J : Precoverage C} [IsStableUnderComposition J] {ι : Type w} {S : C} {X : ι → C} (f : ∀ i, X i ⟶ S) (hf : Presieve.ofArrows X f ∈ J S) diff --git a/Mathlib/Logic/Embedding/Set.lean b/Mathlib/Logic/Embedding/Set.lean index 1eb4b2947b9212..4036dffb4dc419 100644 --- a/Mathlib/Logic/Embedding/Set.lean +++ b/Mathlib/Logic/Embedding/Set.lean @@ -162,6 +162,7 @@ the natural injection from the sigma-type `(i : ι) × ↑(s i)` to `α`. -/ obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩) rfl +set_option warning.simp.otherHead false in @[norm_cast] lemma Function.Embedding.coe_sigmaSet {s : ι → Set α} (h) : (Function.Embedding.sigmaSet h : ((i : ι) × s i) → α) = fun x ↦ x.2.1 := rfl From 4462ca1dfc68ff79c8fbc8ea1b35e67ee9aa1d87 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 13 Apr 2026 13:00:54 +0000 Subject: [PATCH 60/77] chore: silence `varHead` warning --- Mathlib/Probability/Kernel/Defs.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Probability/Kernel/Defs.lean b/Mathlib/Probability/Kernel/Defs.lean index ca32d6bd9fcb3a..2362506ade3a96 100644 --- a/Mathlib/Probability/Kernel/Defs.lean +++ b/Mathlib/Probability/Kernel/Defs.lean @@ -288,11 +288,13 @@ lemma apply_congr_of_mem_measurableAtom (κ : Kernel α β) {y' y : α} (hy' : y ext s hs exact mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl +set_option warning.simp.varHead false in @[nontriviality] lemma eq_zero_of_isEmpty_left (κ : Kernel α β) [h : IsEmpty α] : κ = 0 := by ext a exact h.elim a +set_option warning.simp.varHead false in @[nontriviality] lemma eq_zero_of_isEmpty_right (κ : Kernel α β) [IsEmpty β] : κ = 0 := by ext a From 39ef8defdbea5bf33f00bb4b0f7dff70aec6b0d4 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 13 Apr 2026 13:08:29 +0000 Subject: [PATCH 61/77] chore: fix `globalAtrtributeIn` test --- MathlibTest/globalAttributeIn.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/MathlibTest/globalAttributeIn.lean b/MathlibTest/globalAttributeIn.lean index a61961950ef7e2..56ced2d39e8426 100644 --- a/MathlibTest/globalAttributeIn.lean +++ b/MathlibTest/globalAttributeIn.lean @@ -57,6 +57,7 @@ error: Despite the `in`, the attribute ext is added globally to foo please remove the `in` or make this a `local ext` -/ #guard_msgs in +set_option warning.simp.varHead false in attribute [simp, local simp, ext, scoped instance, -simp, -ext] foo in def bar := False From d04433780ffde215071a2aa2a7ae3a939493ea20 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Mon, 13 Apr 2026 13:58:48 +0000 Subject: [PATCH 62/77] chore: fix `Archive` build --- Archive/Examples/IfNormalization/Result.lean | 1 + Archive/Imo/Imo2024Q6.lean | 2 ++ 2 files changed, 3 insertions(+) diff --git a/Archive/Examples/IfNormalization/Result.lean b/Archive/Examples/IfNormalization/Result.lean index e76444515c5b42..8af518d298d0c3 100644 --- a/Archive/Examples/IfNormalization/Result.lean +++ b/Archive/Examples/IfNormalization/Result.lean @@ -24,6 +24,7 @@ We add some local simp lemmas so we can unfold the definitions of the normalizat attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars List.disjoint +set_option warning.simp.varHead false in attribute [local simp] apply_ite ite_eq_iff' variable {b : Bool} {f : ℕ → Bool} {i : ℕ} {t e : IfExpr} diff --git a/Archive/Imo/Imo2024Q6.lean b/Archive/Imo/Imo2024Q6.lean index 8e26eb7b9494f6..97d7b6d4ed16dd 100644 --- a/Archive/Imo/Imo2024Q6.lean +++ b/Archive/Imo/Imo2024Q6.lean @@ -55,6 +55,7 @@ lemma Aquaesulian.injective : Function.Injective f := by · exact (h.eq_of_apply_eq_inl he.symm hc).symm · exact h.eq_of_apply_eq_inl he hc +set_option warning.simp.varHead false in @[simp] lemma Aquaesulian.apply_zero : f 0 = 0 := by refine h.injective ?_ @@ -68,6 +69,7 @@ lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by · rw [add_neg_cancel, h.apply_zero] at hc exact hc.symm +set_option warning.simp.varHead false in @[simp] lemma Aquaesulian.apply_neg_apply (x : G) : f (-(f x)) = -x := by rw [← add_eq_zero_iff_eq_neg] From f74b5ed4f50b31eaaeaf715070690f63c7f3f548 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 13 Apr 2026 15:14:50 +0000 Subject: [PATCH 63/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13325 --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index f1adde96a1c498..501de355f5e18d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6bd6d39000c7c175ed1cc88f00ef682d31be8b6a", + "rev": "7b47d455134a2bae3f32350389756a731206c86d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13325", From 670c0bf48a617ecb4fc1262c782e363872ea09d4 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 13 Apr 2026 17:11:29 +0000 Subject: [PATCH 64/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/13325 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 501de355f5e18d..2a8214015873a8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7b47d455134a2bae3f32350389756a731206c86d", + "rev": "6b72ff123eeec697911ff4e1bb2b84af54fbe9e7", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-13325", diff --git a/lean-toolchain b/lean-toolchain index 4838ce217e5977..b4b930375c7f7d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13325-89c4bb1 +leanprover/lean4-pr-releases:pr-release-13325-95ecc71 From 2f4e09cdff59cd5482d13e85f635a2e68101f9d0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 13 Apr 2026 22:50:37 +0000 Subject: [PATCH 65/77] fix from nightly-testing --- scripts/create_deprecated_modules.lean | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/scripts/create_deprecated_modules.lean b/scripts/create_deprecated_modules.lean index 17dff24f395335..d17459a8128f45 100644 --- a/scripts/create_deprecated_modules.lean +++ b/scripts/create_deprecated_modules.lean @@ -5,6 +5,7 @@ Authors: Damiano Testa -/ --import Mathlib.Init +import Std.Time.Format import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -- a comment here to test `keepTrailing @@ -49,8 +50,12 @@ It returns just the imports of `fileContent`, including trailing comments if `ke -/ def getHeader (fname fileContent : String) (keepTrailing : Bool) : IO String := do let (stx, _) ← Parser.parseHeader (Parser.mkInputContext fileContent fname) - let stx := if keepTrailing then stx.raw else stx.raw.unsetTrailing - let some substring := stx.getSubstring? | throw <| .userError "No substring: we have a problem!" + let imports := stx.raw.getArg 2 -- extract just the imports list + let imports := if keepTrailing then imports else imports.unsetTrailing + -- Use `withLeading := false` to exclude leading comments (e.g. copyright header) that the + -- parser now attaches to the first token (see leanprover/lean4#12662). + let some substring := imports.getSubstring? (withLeading := false) | + throw <| .userError "No substring: we have a problem!" return substring.toString /-- @@ -371,10 +376,11 @@ replaced by the suggestion, which means that you can click on multiple suggestio the deprecations later on. -/ -#find_deleted_files 0 +-- #find_deleted_files 0 /-- -info: import Std.Time.Zoned +info: import Std.Time.Format +import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -/ #guard_msgs in @@ -384,7 +390,8 @@ run_cmd logInfo head /-- -info: import Std.Time.Zoned +info: import Std.Time.Format +import Std.Time.Zoned import Lean.Meta.Tactic.TryThis -- a comment here to test `keepTrailing -/ From d3e9985046e0fdff2fea7541a0d93e65817a87ac Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Tue, 14 Apr 2026 09:27:55 +0000 Subject: [PATCH 66/77] chore: bump to nightly-2026-04-14 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index eb7023afec000d..8db80a7b77a650 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-13 +leanprover/lean4:nightly-2026-04-14 From 606f569015f01c9d4e70974b3be8467f2fc5ab1a Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Wed, 15 Apr 2026 09:28:48 +0000 Subject: [PATCH 67/77] chore: bump to nightly-2026-04-15 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 8db80a7b77a650..b74ced19101876 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-14 +leanprover/lean4:nightly-2026-04-15 From 9e7eebd31d71e2faaf8c58aaa13da435a5595805 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 16 Apr 2026 08:02:46 +0000 Subject: [PATCH 68/77] fixes --- Mathlib/Analysis/Distribution/Distribution.lean | 2 +- Mathlib/CategoryTheory/Types/Basic.lean | 2 +- Mathlib/RingTheory/Perfection.lean | 2 ++ 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Distribution/Distribution.lean b/Mathlib/Analysis/Distribution/Distribution.lean index 931ea029f07803..c392c764bd5753 100644 --- a/Mathlib/Analysis/Distribution/Distribution.lean +++ b/Mathlib/Analysis/Distribution/Distribution.lean @@ -192,7 +192,7 @@ end mapCLM section DiracDelta /-- The Dirac delta distribution. This is zero if `x` does not belong to `Ω`. -/ -def delta (x : E) : 𝓓'^{n}(Ω, ℝ) where +noncomputable def delta (x : E) : 𝓓'^{n}(Ω, ℝ) where toFun f := f x map_add' _ _ := rfl map_smul' _ _ := rfl diff --git a/Mathlib/CategoryTheory/Types/Basic.lean b/Mathlib/CategoryTheory/Types/Basic.lean index 8701000d99dc29..5de3f5b72f7cb6 100644 --- a/Mathlib/CategoryTheory/Types/Basic.lean +++ b/Mathlib/CategoryTheory/Types/Basic.lean @@ -315,7 +315,7 @@ Write this as `uliftFunctor.{5, 2}` to get `Type 2 ⥤ Type 5`. @[pp_with_univ, simps obj map] def uliftFunctor : Type u ⥤ Type max u v where obj X := ULift.{v} X - map {X} {_} f := fun x : ULift.{v} X => ULift.up (f x.down) + map {X} {_} f := fun x : ULift.{v} X => ULift.up.{v} (f x.down) @[simp] theorem uliftFunctor_obj {X : Type u} : uliftFunctor.{v}.obj X = ULift.{v} X := diff --git a/Mathlib/RingTheory/Perfection.lean b/Mathlib/RingTheory/Perfection.lean index 4a4117cdd01125..b705efb5863b4c 100644 --- a/Mathlib/RingTheory/Perfection.lean +++ b/Mathlib/RingTheory/Perfection.lean @@ -838,6 +838,8 @@ namespace Tilt noncomputable instance [Fact p.Prime] [hvp : Fact (v p ≠ 1)] : Field (Tilt K v O hv p) := haveI := Fact.mk <| mt hv.one_of_isUnit <| (map_natCast (algebraMap O K) p).symm ▸ hvp.1 haveI := PreTilt.isDomain K v O hv p + #adaptation_note /-- This `letI` was not needed prior to nightly-2026-04-15. -/ + letI : CommRing (PreTilt O p) := inferInstance inferInstanceAs <| Field (FractionRing _) end Tilt From 8ba95847a2694c66068b94275efe201a1fcde041 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 16 Apr 2026 08:05:17 +0000 Subject: [PATCH 69/77] fix --- Mathlib/CategoryTheory/Types/Basic.lean | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/Mathlib/CategoryTheory/Types/Basic.lean b/Mathlib/CategoryTheory/Types/Basic.lean index 5de3f5b72f7cb6..ea2397b985dca9 100644 --- a/Mathlib/CategoryTheory/Types/Basic.lean +++ b/Mathlib/CategoryTheory/Types/Basic.lean @@ -315,16 +315,7 @@ Write this as `uliftFunctor.{5, 2}` to get `Type 2 ⥤ Type 5`. @[pp_with_univ, simps obj map] def uliftFunctor : Type u ⥤ Type max u v where obj X := ULift.{v} X - map {X} {_} f := fun x : ULift.{v} X => ULift.up.{v} (f x.down) - -@[simp] -theorem uliftFunctor_obj {X : Type u} : uliftFunctor.{v}.obj X = ULift.{v} X := - rfl - -@[simp] -theorem uliftFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : ULift.{v} X) : - uliftFunctor.map f x = ULift.up (f x.down) := - rfl + map {X} {_} f := TypeCat.ofHom fun x : ULift.{v} X => ULift.up.{v} (f x.down) /-- `uliftFunctor : Type u ⥤ Type max u v` is fully faithful. -/ def fullyFaithfulULiftFunctor : (uliftFunctor.{v, u}).FullyFaithful where From f9ae5cc6f301a0a0e6091e8e5c9c3d501b9812f8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 16 Apr 2026 09:28:08 +0000 Subject: [PATCH 70/77] fixes --- Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean | 2 +- Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean | 4 ++-- Mathlib/CategoryTheory/Sites/Sieves.lean | 2 +- Mathlib/RingTheory/Flat/Rank.lean | 1 + 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean index e593c19088e76d..4778e592b7948a 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean @@ -141,7 +141,7 @@ noncomputable instance monoidalCategory : open BraidedCategory -instance symmetricCategory : +noncomputable instance symmetricCategory : SymmetricCategory (PresheafOfModules.{u} (R ⋙ forget₂ _ _)) where braiding M₁ M₂ := isoMk (fun X ↦ braiding (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X)) diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean index 70e0fbfb413bf6..a7c651c699abb9 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean @@ -94,7 +94,7 @@ lemma horn_obj_eq_univ {n : ℕ} (i : Fin (n + 1)) (m : ℕ) (h : m + 1 < n := b Finset.card_singleton, add_le_add_iff_right] at this have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le lia - have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm.{u} f) i = j := + have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.{u}.symm f) i = j := ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩ simpa [horn_eq_iSup] using this @@ -140,7 +140,7 @@ lemma face_le_horn_iff {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)) : lemma objEquiv_symm_notMem_horn_of_isIso {n : ℕ} (i : Fin (n + 1)) {d : SimplexCategory} (f : d ⟶ ⦋n⦌) [IsIso f] : - stdSimplex.objEquiv.symm.{u} f ∉ Λ[n, i].obj (op d) := by + stdSimplex.objEquiv.{u}.symm f ∉ Λ[n, i].obj (op d) := by rw [mem_horn_iff, ne_eq, not_not] ext i simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩ diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index a6fb9bc171af42..5715339400c477 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/Mathlib/CategoryTheory/Sites/Sieves.lean @@ -1263,7 +1263,7 @@ def uliftFunctorInclusion (S : Sieve X) : @[simps] def toUliftFunctor (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S f) : uliftYoneda.{w}.obj Y ⟶ Sieve.uliftFunctor.{w} S where - app Z g := ⟨g.down ≫ f, S.downward_closed hf g.down⟩ + app Z := TypeCat.ofHom fun g ↦ ⟨g.down ≫ f, S.downward_closed hf g.down⟩ theorem uliftNatTransOfLe_comm {S T : Sieve X} (h : S ≤ T) : uliftNatTransOfLe.{w} h ≫ uliftFunctorInclusion.{w} _ = uliftFunctorInclusion.{w} _ := diff --git a/Mathlib/RingTheory/Flat/Rank.lean b/Mathlib/RingTheory/Flat/Rank.lean index a7a380d3a50fdb..7f5eae009c9a13 100644 --- a/Mathlib/RingTheory/Flat/Rank.lean +++ b/Mathlib/RingTheory/Flat/Rank.lean @@ -36,6 +36,7 @@ attribute [local instance] Module.free_of_flat_of_isLocalRing variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S] +set_option backward.isDefEq.respectTransparency false in lemma PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap (p : PrimeSpectrum R) : 0 < Module.rankAtStalk (R := R) S p ↔ p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) := by rw [Module.rankAtStalk_eq, Module.finrank_pos_iff, p.nontrivial_iff_mem_rangeComap] From cecf37bdace26a422cf4eb0059fb7f0d410969b6 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Thu, 16 Apr 2026 09:31:37 +0000 Subject: [PATCH 71/77] chore: bump to nightly-2026-04-16 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b74ced19101876..844e3659d22483 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-15 +leanprover/lean4:nightly-2026-04-16 From c33286bef8c14a6fce87ea5fdd7f2bd196a30577 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 17 Apr 2026 19:04:23 +1000 Subject: [PATCH 72/77] fix upstreamed import --- Mathlib/Order/Bounded.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Order/Bounded.lean b/Mathlib/Order/Bounded.lean index dddc3d771498da..6ab52893a60e3b 100644 --- a/Mathlib/Order/Bounded.lean +++ b/Mathlib/Order/Bounded.lean @@ -5,7 +5,6 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.Tactic.Linter.DeprecatedModule public import Mathlib.Order.RelClasses public import Mathlib.Order.Interval.Set.Basic public import Mathlib.Order.Bounds.Defs From bba4e0716004d5583247ab95fc436e817087e83a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 17 Apr 2026 22:22:42 +1000 Subject: [PATCH 73/77] set_option --- Mathlib/RingTheory/Flat/Rank.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/RingTheory/Flat/Rank.lean b/Mathlib/RingTheory/Flat/Rank.lean index a7a380d3a50fdb..7f5eae009c9a13 100644 --- a/Mathlib/RingTheory/Flat/Rank.lean +++ b/Mathlib/RingTheory/Flat/Rank.lean @@ -36,6 +36,7 @@ attribute [local instance] Module.free_of_flat_of_isLocalRing variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S] +set_option backward.isDefEq.respectTransparency false in lemma PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap (p : PrimeSpectrum R) : 0 < Module.rankAtStalk (R := R) S p ↔ p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) := by rw [Module.rankAtStalk_eq, Module.finrank_pos_iff, p.nontrivial_iff_mem_rangeComap] From a450fa064ebfe9a474d5fd2f5113b095e71bbc6c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 18 Apr 2026 08:18:58 +1000 Subject: [PATCH 74/77] fixes --- Mathlib/CategoryTheory/Sites/Sieves.lean | 2 +- MathlibTest/DocPrime.lean | 7 +++++-- MathlibTest/LintStyle.lean | 3 ++- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index 84c4db3b3add33..aaa29a83dcfec3 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/Mathlib/CategoryTheory/Sites/Sieves.lean @@ -1263,7 +1263,7 @@ def uliftFunctorInclusion (S : Sieve X) : @[simps] def toUliftFunctor (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S f) : uliftYoneda.{w}.obj Y ⟶ Sieve.uliftFunctor.{w} S where - app Z g := TypeCat.ofHom fun g ↦ ⟨g.down ≫ f, S.downward_closed hf g.down⟩ + app Z := TypeCat.ofHom fun g ↦ ⟨g.down ≫ f, S.downward_closed hf g.down⟩ theorem uliftNatTransOfLe_comm {S T : Sieve X} (h : S ≤ T) : uliftNatTransOfLe.{w} h ≫ uliftFunctorInclusion.{w} _ = uliftFunctorInclusion.{w} _ := diff --git a/MathlibTest/DocPrime.lean b/MathlibTest/DocPrime.lean index 7411651cca5259..bc217c8686bc65 100644 --- a/MathlibTest/DocPrime.lean +++ b/MathlibTest/DocPrime.lean @@ -60,6 +60,9 @@ Note: This linter can be disabled with `set_option linter.docPrime false` @[simp] theorem thm_with_attr_no_doc' : True := .intro +class Dummy where + field : True + /-- warning: `inst_no_doc'` is missing a doc-string, please add one. Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible. @@ -67,7 +70,7 @@ Declarations whose name ends with a `'` are expected to contain an explanation f Note: This linter can be disabled with `set_option linter.docPrime false` -/ #guard_msgs in -instance inst_no_doc' : True := .intro +instance inst_no_doc' : Dummy := ⟨.intro⟩ /-- warning: `abbrev_no_doc'` is missing a doc-string, please add one. @@ -91,6 +94,6 @@ def def_no_doc' : True := .intro namespace Foo' example : True := .intro -instance : True := .intro +instance : Dummy := ⟨.intro⟩ end Foo' diff --git a/MathlibTest/LintStyle.lean b/MathlibTest/LintStyle.lean index 4e9351942fc5c0..e6cd6fb7f83b58 100644 --- a/MathlibTest/LintStyle.lean +++ b/MathlibTest/LintStyle.lean @@ -284,7 +284,8 @@ warning: Please use '<|' instead of '$' for the pipe operator. Note: This linter can be disabled with `set_option linter.style.dollarSyntax false` -/ #guard_msgs in -instance (f g : Nat → Nat) : Inhabited Nat where +@[reducible] +def test (f g : Nat → Nat) : Inhabited Nat where default := by · have := 0 · have : Nat := f $ g $ 0 From e479388d393de50704b991888f076be362d259ef Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 18 Apr 2026 08:20:28 +1000 Subject: [PATCH 75/77] fixes --- Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean | 4 ++-- MathlibTest/ToDual.lean | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean index 70e0fbfb413bf6..a7c651c699abb9 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean @@ -94,7 +94,7 @@ lemma horn_obj_eq_univ {n : ℕ} (i : Fin (n + 1)) (m : ℕ) (h : m + 1 < n := b Finset.card_singleton, add_le_add_iff_right] at this have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le lia - have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm.{u} f) i = j := + have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.{u}.symm f) i = j := ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩ simpa [horn_eq_iSup] using this @@ -140,7 +140,7 @@ lemma face_le_horn_iff {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)) : lemma objEquiv_symm_notMem_horn_of_isIso {n : ℕ} (i : Fin (n + 1)) {d : SimplexCategory} (f : d ⟶ ⦋n⦌) [IsIso f] : - stdSimplex.objEquiv.symm.{u} f ∉ Λ[n, i].obj (op d) := by + stdSimplex.objEquiv.{u}.symm f ∉ Λ[n, i].obj (op d) := by rw [mem_horn_iff, ne_eq, not_not] ext i simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩ diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean index b9bb47f4ad4a2b..d3139be878fdc1 100644 --- a/MathlibTest/ToDual.lean +++ b/MathlibTest/ToDual.lean @@ -31,6 +31,7 @@ structure Lattice (α : Type) extends SemilatticeInf α, SemilatticeSup α attribute [to_dual existing] Lattice.toSemilatticeInf +set_option linter.impossibleInstance false in -- we can reorder arguments of arguments in `SemilatticeInf.mk` @[to_dual] instance [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where From d33ab3c2f6868cec700797a06ded94870a2facc5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 18 Apr 2026 08:33:12 +1000 Subject: [PATCH 76/77] fixes --- MathlibTest/ToDual.lean | 1 - lake-manifest.json | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean index d3139be878fdc1..b9bb47f4ad4a2b 100644 --- a/MathlibTest/ToDual.lean +++ b/MathlibTest/ToDual.lean @@ -31,7 +31,6 @@ structure Lattice (α : Type) extends SemilatticeInf α, SemilatticeSup α attribute [to_dual existing] Lattice.toSemilatticeInf -set_option linter.impossibleInstance false in -- we can reorder arguments of arguments in `SemilatticeInf.mk` @[to_dual] instance [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where diff --git a/lake-manifest.json b/lake-manifest.json index a368a0a46ff776..96cf216690b058 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3b89330c9c0ccaeed89cf99b2cd292722e3495c9", + "rev": "4b591181697264394a76288a163fd1d47621c96e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From 4f40f6e9ea040b62de44119404d38ef214b7efda Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 18 Apr 2026 09:15:56 +1000 Subject: [PATCH 77/77] fix Init filter in MinImports --- Mathlib/Tactic/Linter/MinImports.lean | 4 ++-- Mathlib/Tactic/MinImports.lean | 9 ++++++++- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index ae2a42c439c518..ddfbb78c56a2a2 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -125,7 +125,7 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do -- when the linter reaches the end of the file or `#exit`, it gives a report if #[``Parser.Command.eoi, ``Lean.Parser.Command.exit].contains stx.getKind then let explicitImportsInFile : NameSet := - .ofArray ((env.imports.map (·.module)).erase `Init) + .ofArray ((env.imports.map (·.module)).filter (!isInitImport ·)) let newImps := importsSoFar \ explicitImportsInFile let currentlyUnneededImports := explicitImportsInFile \ importsSoFar -- we read the current file, to do a custom parsing of the imports: @@ -146,7 +146,7 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do logWarningAt ((impMods.raw.find? (·.isOfKind `import)).getD default) m!"-- missing imports\n{"\n".intercalate withImport.toList}" let id ← getId stx - let newImports := getIrredundantImports env (← getAllImports stx id) + let newImports := (getIrredundantImports env (← getAllImports stx id)).filter (!isInitImport ·) let tot := (newImports.append importsSoFar) let redundant := env.findRedundantImports tot.toArray let currImports := tot \ redundant diff --git a/Mathlib/Tactic/MinImports.lean b/Mathlib/Tactic/MinImports.lean index 9d5f781fece6ed..732ae93bb3ddda 100644 --- a/Mathlib/Tactic/MinImports.lean +++ b/Mathlib/Tactic/MinImports.lean @@ -64,6 +64,13 @@ open Lean Elab Command namespace Mathlib.Command.MinImports +/-- Returns `true` if `n` is `Init` or a descendant of `Init`. These imports are always available +in ordinary Mathlib files, so they are omitted from user-facing `#min_imports` output. -/ +partial def isInitImport : Name → Bool + | `Init => true + | .str p _ => isInitImport p + | _ => false + /-- `getSyntaxNodeKinds stx` takes a `Syntax` input `stx` and returns the `NameSet` of all the `SyntaxNodeKinds` and all the identifiers contained in `stx`. -/ partial @@ -251,7 +258,7 @@ It is used to provide the internally generated name for "nameless" `instance`s. -/ def minImpsCore (stx id : Syntax) : CommandElabM Unit := do let tot := getIrredundantImports (← getEnv) (← getAllImports stx id) - let fileNames := tot.toArray.qsort Name.lt + let fileNames := (tot.toArray.filter (!isInitImport ·)).qsort Name.lt logInfoAt (← getRef) m!"{"\n".intercalate (fileNames.map (s!"public import {·}")).toList}" /-- `#min_imports in cmd` scans the syntax `cmd` and the declaration obtained by elaborating `cmd`