chore: bump to v4.25.0-rc1 (#756)

Closes #733.

Author: pitmonticone

FLT/Patching/Module.lean

@@ -59,8 +59,8 @@ lemma Module.UniformlyBoundedRank.exists_finsupp_surjective (i) :
     · exact (Fin.castLE_injective _).comp (Fintype.equivFin _).injective
   · simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective]
     refine (Finsupp.mapRange_surjective _ (map_zero _) Ideal.Quotient.mk_surjective).comp ?_
-    exact Finsupp.comapDomain_surjective _ ((Fin.castLE_injective _).comp
-      (Fintype.equivFin _).injective)
+    exact Finsupp.comapDomain_surjective
+      ((Fin.castLE_injective _).comp (Fintype.equivFin _).injective)
 
 lemma Module.UniformlyBoundedRank.finite_quotient_smul (i) (I : Ideal R) [Finite (R ⧸ I)] :
     Finite (M i ⧸ (I • ⊤ : Submodule R (M i))) := by

FLT/Patching/Utils/Lemmas.lean

@@ -310,16 +310,6 @@ lemma Pi.liftQuotientₗ_bijective {ι R M : Type*} [CommRing R] [AddCommGroup M
     smul_apply, Algebra.linearMap_apply, Ideal.Quotient.algebraMap_eq, zero_apply,
     Ideal.Quotient.eq_zero_iff_mem, smul_eq_mul, I.mul_mem_right _ hr, implies_true]
 
-lemma Finsupp.comapDomain_surjective {α β M} [Zero M] [Finite β]
-    (f : α → β) (hf : Function.Injective f) :
-    Function.Surjective fun l : β →₀ M ↦ Finsupp.comapDomain f l hf.injOn := by
-  classical
-  intro x
-  cases isEmpty_or_nonempty α
-  · refine ⟨0, Finsupp.ext <| fun a ↦ IsEmpty.elim ‹_› a⟩
-  obtain ⟨g, hg⟩ := hf.hasLeftInverse
-  refine ⟨Finsupp.equivFunOnFinite.symm (x ∘ g), Finsupp.ext <| fun a ↦ by simp [hg a]⟩
-
 lemma IsModuleTopology.compactSpace
     (R M : Type*) [CommRing R] [TopologicalSpace R] [AddCommGroup M]
     [Module R M] [TopologicalSpace M] [IsModuleTopology R M]

lake-manifest.json

@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
+   "rev": "da2fd30c91aa177fc00c364d00e2c55334a5b32b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0",
+   "inputRev": "v4.25.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
+   "rev": "7607162f5a1c1eb23c23027629a418b3a160670e",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "e5c37730d22634ee0169c164f25dac49918ed951",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.77",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "cbe864cd5177966c9e005418cfdc1fb36db62e13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
+   "rev": "593aa51c4aa07ee81e9233b53e1f61a5b4d9f761",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "5bd478197f2e5d2a4fde527cf3581d83f49baa9b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "f75f4926aff7ba19949e16c19094d7298806b1a6",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",

lakefile.toml

@@ -15,7 +15,7 @@ warn.sorry = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.24.0"
+rev = "v4.25.0-rc1"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0-rc1