feat: bump to v4.25.0-rc2

Poly.lean

@@ -2,9 +2,7 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Distributivity
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf
--- import Poly.LCCC.BeckChevalley
--- import Poly.LCCC.Presheaf
--- import Poly.Type.Univariate
--- import Poly.Exponentiable
-import Poly.UvPoly.Basic
+import Poly.Type.Univariate
+import Poly.UvPoly.Limits
+import Poly.UvPoly.UPIso
 import Poly.MvPoly.Basic

Poly/Bifunctor/Sigma.lean

@@ -5,8 +5,7 @@ Authors: Wojciech Nawrocki
 -/
 import Mathlib.CategoryTheory.Comma.Over.Basic
 import Mathlib.CategoryTheory.Functor.Currying
-
-import SEq.Tactic.DepRewrite
+import Mathlib.Tactic.DepRewrite
 
 import Poly.ForMathlib.CategoryTheory.Elements
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
@@ -178,5 +177,3 @@ def forget_iso_Sigma (A : 𝒞) :
       simp
 
 end CategoryTheory.Over
-
-#min_imports

Poly/ForMathlib/CategoryTheory/Elements.lean

@@ -22,7 +22,7 @@ theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) :
 theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) eq :
     G.map (Y := ⟨Z, F.map g (F.map f a)⟩) (Subtype.mk (α := X ⟶ Z) (f ≫ g) eq) =
     G.map (X := ⟨X, a⟩) (Y := ⟨Y, F.map f a⟩) (Subtype.mk (α := X ⟶ Y) f rfl) ≫
-    G.map (Subtype.mk (α := Y ⟶ Z) g (rfl)) := by
+    G.map (Subtype.mk g rfl) := by
   set X : F.Elements := ⟨X, a⟩
   set Y : F.Elements := ⟨Y, F.map f a⟩
   set Z : F.Elements := ⟨Z, F.map g (F.map f a)⟩

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean

@@ -315,12 +315,12 @@ theorem pullbackMapTwoSquare_app :
   aesop
 
 theorem forget_map_pullbackMapTwoSquare :
-    (forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) =
+    (Over.forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) =
     pullback.map _ _ _ _ (𝟙 _) h k (id_comp _).symm sq.w.symm := by
   simp only [forget_map, pullbackMapTwoSquare_app, homMk_left]
 
 theorem isIso_forgetMappullbackMapTwoSquare_of_isPullback (pb : IsPullback h f g k) :
-    IsIso ((forget Z).map ((pullbackMapTwoSquare h f g k pb.toCommSq).app A)) := by
+    IsIso ((Over.forget Z).map ((pullbackMapTwoSquare h f g k pb.toCommSq).app A)) := by
   rw [forget_map_pullbackMapTwoSquare (sq:= pb.toCommSq)]
   let paste_horiz_pb := paste_horiz (IsPullback.of_hasPullback f A.hom) pb
   apply pullback.map_isIso_of_pullback_right_of_comm_cube
@@ -333,7 +333,7 @@ instance pullbackMapTwoSquare_of_isPullback_isIso (pb : IsPullback h f g k) :
   apply (config := { allowSynthFailures:= true}) NatIso.isIso_of_isIso_app
   intro A
   have := isIso_forgetMappullbackMapTwoSquare_of_isPullback A pb
-  exact ReflectsIsomorphisms.reflects (forget Z)
+  exact ReflectsIsomorphisms.reflects (Over.forget Z)
     ((pullbackMapTwoSquare h f g k pb.toCommSq).app A)
 
 /-- The pullback-map exchange isomorphism. -/

Poly/ForMathlib/CategoryTheory/Types.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 
-import Mathlib.CategoryTheory.Types
+import Mathlib.CategoryTheory.Types.Basic
 
 namespace CategoryTheory.FunctorToTypes
 

Poly/Type/Univariate.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour
 -/
 
-import Mathlib.CategoryTheory.Types
+import Mathlib.CategoryTheory.Types.Basic
 
 open CategoryTheory Category Functor
 

Poly/UvPoly/UPIso.lean

@@ -20,7 +20,7 @@ This is equivalent to the type of partial product cones with apex `Γ` over `X`.
 def partProdsOver : Cᵒᵖ ⥤ C ⥤ Type v :=
   Functor.Sigma
     ((Over.equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙
-      (forget E).op ⋙ coyoneda (C := C))
+      (Over.forget E).op ⋙ coyoneda (C := C))
 
 @[simp]
 theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.partProdsOver.obj Γ).obj X) :
@@ -40,7 +40,7 @@ def iso_Sigma (P : UvPoly E B) :
     P.functor ⋙₂ coyoneda (C := C) ≅ P.partProdsOver :=
   calc
     P.functor ⋙₂ coyoneda (C := C) ≅
-        (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) :=
+        (star E ⋙ pushforward P.p) ⋙₂ (Over.forget B ⋙₂ coyoneda (C := C)) :=
       Iso.refl _
 
     _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma
@@ -63,7 +63,7 @@ def iso_Sigma (P : UvPoly E B) :
           _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) :=
             Iso.refl _
 
-          _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) :=
+          _ ≅ (Over.pullback P.p).op ⋙ (Over.forget E).op ⋙ coyoneda (C := C) :=
             isoWhiskerLeft (Over.pullback P.p).op (Adjunction.coyoneda_iso <| forgetAdjStar E).symm;
 
       Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i)
@@ -75,7 +75,6 @@ theorem equiv_app (Γ X : C) (be : Γ ⟶ P.functor.obj X) :
     P.equiv Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by
   dsimp [equiv]
 
--- TODO(WN): Checking the theorem statement takes 5s, and kernel typechecking 10s!
 lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) :
     P.equiv Δ X (σ ≫ be) =
       let p := P.equiv Γ X be
@@ -84,7 +83,7 @@ lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.
   conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_left, ← equiv_app]
   simp
 
--- TODO(WN): Kernel typechecking takes 10s!
+-- NOTE(WN): As of Lean 4.25, kernel typechecking time is down to 1s from 10s?!
 lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) :
     equiv P Γ Y (be ≫ P.functor.map f) =
       let p := equiv P Γ X be

lake-manifest.json

@@ -11,21 +11,11 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/Vtec234/lean4-seq",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "7279fc299b10681b00aefe1edd0668766cead87c",
-   "name": "seq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "839e741740619e20759a7153fd93b5c7d8df13e0",
+   "rev": "32bd6c7c8ca4a4be1c71bc04df0c9cf929d04818",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
+   "rev": "8864a73bf79aad549e34eff972c606343935106d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7c02243c07b61d493d7607ede432026781a3e47c",
+   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
+   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.71",
+   "inputRev": "v0.0.77",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
+   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
+   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a9a0cb7672b7134497c9d813e53999c9311f4037",
+   "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
+   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",

lakefile.lean

@@ -11,8 +11,6 @@ package Poly where
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
-require seq from git "https://github.com/Vtec234/lean4-seq"
-
 @[default_target]
 lean_lib Poly where
   -- add any library configuration options here
@@ -21,4 +19,4 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.23.0-rc2"
+  "https://github.com/leanprover/doc-gen4" @ "v4.25.0-rc2"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.23.0-rc2
+leanprover/lean4:v4.25.0-rc2