From 8d08e270ece92c1a812fbbca183872691c19f542 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Apr 2026 14:35:06 +1000 Subject: [PATCH 01/10] 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 02/10] 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 03/10] 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 04/10] 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 05/10] 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 06/10] 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 07/10] touch for CI From 85c19f239fc3a167a10e676314e00d305d2d4df9 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Tue, 7 Apr 2026 08:32:32 +0000 Subject: [PATCH 08/10] 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 09/10] 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 10/10] chore: adaptations for nightly-2026-04-07