From 9e45c207936fe83e1de9fc69b881322b919d1f71 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 15:38:05 +1100 Subject: [PATCH 1/2] chore: bump to latest Mathlib and v4.15.0-rc1 toolchain --- .../FiniteAdeleRing/BaseChange.lean | 1 + FLT/ForMathlib/ActionTopology.lean | 2 +- FLT/GlobalLanglandsConjectures/GLnDefs.lean | 2 +- FLT/GlobalLanglandsConjectures/GLzero.lean | 2 +- FLT/MathlibExperiments/Coalgebra/Monoid.lean | 9 +- lake-manifest.json | 88 +++++-------------- lean-toolchain | 2 +- 7 files changed, 36 insertions(+), 70 deletions(-) diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index a3ad747e..02d15a84 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -236,6 +236,7 @@ lemma adicCompletionComapAlgHom_coe (adicCompletionComapAlgHom A K L B v w hvw).commutes _ -- this name is surely wrong +omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] in open WithZeroTopology in lemma v_adicCompletionComapAlgHom (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) (x) : diff --git a/FLT/ForMathlib/ActionTopology.lean b/FLT/ForMathlib/ActionTopology.lean index 2f0d8789..b8c26cd6 100644 --- a/FLT/ForMathlib/ActionTopology.lean +++ b/FLT/ForMathlib/ActionTopology.lean @@ -323,7 +323,7 @@ theorem coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective · apply @Continuous.prodMap _ _ _ _ (_) (_) (_) (_) <;> · rw [continuous_iff_coinduced_le, isActionTopology R A]; rfl · rw [← isActionTopology R A] - exact coinduced_prod_eq_prod_coinduced φ φ hφ hφ + exact coinduced_prod_eq_prod_coinduced (X := A) (Y := A) (S := B) (T := B) φ φ hφ hφ end surjection diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean index d51c8134..d57b2193 100644 --- a/FLT/GlobalLanglandsConjectures/GLnDefs.lean +++ b/FLT/GlobalLanglandsConjectures/GLnDefs.lean @@ -80,7 +80,7 @@ open scoped nonZeroDivisors noncomputable instance foobar37 : Algebra R (FiniteAdeleRing R K) := RingHom.toAlgebra ((algebraMap K (FiniteAdeleRing R K)).comp (algebraMap R K)) -@[deprecated mul_nonZeroDivisor_mem_finiteIntegralAdeles] +@[deprecated mul_nonZeroDivisor_mem_finiteIntegralAdeles (since := "2024-08-11")] lemma FiniteAdeleRing.clear_denominator (a : FiniteAdeleRing R K) : ∃ (b : R⁰) (c : R_hat R K), a * (b : R) = c := by exact mul_nonZeroDivisor_mem_finiteIntegralAdeles a diff --git a/FLT/GlobalLanglandsConjectures/GLzero.lean b/FLT/GlobalLanglandsConjectures/GLzero.lean index 6a138238..085304e5 100644 --- a/FLT/GlobalLanglandsConjectures/GLzero.lean +++ b/FLT/GlobalLanglandsConjectures/GLzero.lean @@ -62,7 +62,7 @@ def ofComplex (c : ℂ) : AutomorphicFormForGLnOverQ 0 ρ := { loc_cst := by rw [IsLocallyConstant] aesop - smooth := by simp [smooth_const] + smooth := by simp [contMDiff_const] } is_periodic := by simp is_slowly_increasing := by diff --git a/FLT/MathlibExperiments/Coalgebra/Monoid.lean b/FLT/MathlibExperiments/Coalgebra/Monoid.lean index 4a029406..6f833a5a 100644 --- a/FLT/MathlibExperiments/Coalgebra/Monoid.lean +++ b/FLT/MathlibExperiments/Coalgebra/Monoid.lean @@ -122,7 +122,10 @@ noncomputable instance instMonoid : Monoid (LinearPoint R A L) where one_mul := one_mul' mul_one := mul_one' -attribute [deprecated] mul_assoc' mul_one' one_mul' mul_repr' +attribute [deprecated mul_assoc (since := "2024-03-10")] mul_assoc' +attribute [deprecated mul_one (since := "2024-03-10")] mul_one' +attribute [deprecated one_mul (since := "2024-03-10")] one_mul' +attribute [deprecated mul_repr (since := "2024-03-10")] mul_repr' end LinearPoint @@ -200,7 +203,9 @@ noncomputable instance instMonoid : Monoid (AlgHomPoint R A L) where one_mul := one_mul' mul_one := mul_one' -attribute [deprecated] mul_assoc' mul_one' one_mul' +attribute [deprecated mul_assoc (since := "2024-03-10")] mul_assoc' +attribute [deprecated mul_one (since := "2024-03-10")] mul_one' +attribute [deprecated one_mul (since := "2024-03-10")] one_mul' section commutative_bialgebra diff --git a/lake-manifest.json b/lake-manifest.json index cc7dc15c..17ebcc91 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,11 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", - "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce", + "rev": "8e459c606cbf19248c6a59956570f051f05e6067", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,60 +15,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "cee87aa25cfbd8e4c3cd89bc26cce86e927e36dc", + "rev": "41ff1f7899c971f91362710d4444e338b8acd644", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -95,49 +45,59 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "119b022b3ea88ec810a677888528e50f8144a26e", + "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1383e72b40dd62a566896a6e348ffe868801b172", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.46", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "de91b59101763419997026c35a41432ac8691f15", + "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f46c0445cc86ad2bc973edf8c5b2bd88bd91913b", + "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.14.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], diff --git a/lean-toolchain b/lean-toolchain index 6d9e70f7..cf25a981 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc3 +leanprover/lean4:v4.15.0-rc1 From c2d710596a174c140c0e61d493e6bf096742a62b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 2 Dec 2024 06:25:50 +0100 Subject: [PATCH 2/2] Update lake-manifest.json --- lake-manifest.json | 62 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 51 insertions(+), 11 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 17ebcc91..56490466 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/PatrickMassot/checkdecls.git", + [{"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "099b90e374ba73983c3fda87595be625f1931669", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", @@ -21,6 +31,46 @@ "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, @@ -90,16 +140,6 @@ "manifestFile": "lake-manifest.json", "inputRev": "v4.14.0", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, "configFile": "lakefile.toml"}], "name": "FLT", "lakeDir": ".lake"}