From c26e710a750cb9d769ee51d0b1b737f9eb437700 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Feb 2026 22:04:58 -0500 Subject: [PATCH] feat: bump to Lean v4.28.0-rc1 --- .../CategoryTheory/Comma/Over/Basic.lean | 4 --- .../CategoryTheory/Comma/Over/Pullback.lean | 12 ++----- .../CategoryTheory/Comma/Over/Sections.lean | 33 ++++++++++--------- .../{CommSq.lean => IsPullback/Basic.lean} | 2 +- .../LocallyCartesianClosed/Basic.lean | 21 ++++++------ .../LocallyCartesianClosed/BeckChevalley.lean | 2 +- .../LocallyCartesianClosed/Presheaf.lean | 6 ++-- Poly/ForMathlib/CategoryTheory/NatTrans.lean | 2 +- .../CategoryTheory/PartialProduct.lean | 4 ++- Poly/Type/Univariate.lean | 2 +- lake-manifest.json | 20 +++++------ lean-toolchain | 2 +- 12 files changed, 52 insertions(+), 58 deletions(-) rename Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/{CommSq.lean => IsPullback/Basic.lean} (93%) diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean index c7d37a7..0abbddf 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean @@ -35,10 +35,6 @@ lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) := rfl -@[simp] -theorem mkIdTerminal_from_left {B : T} (U : Over B) : (mkIdTerminal.from U).left = U.hom := by - simp [mkIdTerminal, CostructuredArrow.mkIdTerminal, Limits.IsTerminal.from, Functor.preimage] - /-- `Over.Sigma Y U` is a shorthand for `(Over.map Y.hom).obj U`. This is a category-theoretic analogue of `Sigma` for types. -/ abbrev Sigma {X : T} (Y : Over X) (U : Over (Y.left)) : Over X := diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean index 111dcec..d5569d6 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean @@ -9,7 +9,7 @@ import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic import Mathlib.CategoryTheory.Monad.Products import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic import Poly.ForMathlib.CategoryTheory.NatTrans -import Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic noncomputable section @@ -19,7 +19,7 @@ namespace CategoryTheory open Category Limits Comonad MonoidalCategory CartesianMonoidalCategory -attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts variable {C : Type u₁} [Category.{v₁} C] @@ -211,7 +211,7 @@ lemma star_map [HasBinaryProducts C] {X : C} {Y Z : C} (f : Y ⟶ Z) : instance [HasBinaryProducts C] (X : C) : (forget X).IsLeftAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩ -attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts lemma whiskerLeftProdMapId [HasFiniteLimits C] {X : C} {A A' : C} {g : A ⟶ A'} : X ◁ g = prod.map (𝟙 X) g := by @@ -298,12 +298,6 @@ def starIsoToOverTerminal [HasTerminal C] [HasBinaryProducts C] : variable {C} -/-- A natural isomorphism between the functors `star X` and `star Y ⋙ pullback f` -for any morphism `f : X ⟶ Y`. -/ -def starPullbackIsoStar [HasBinaryProducts C] [HasPullbacks C] {X Y : C} (f : X ⟶ Y) : - star Y ⋙ pullback f ≅ star X := - conjugateIsoEquiv ((mapPullbackAdj f).comp (forgetAdjStar Y)) (forgetAdjStar X) (mapForget f) - /-- The functor `Over.pullback f : Over Y ⥤ Over X` is naturally isomorphic to `Over.star : Over Y ⥤ Over (Over.mk f)` post-composed with the iterated slice equivlanece `Over (Over.mk f) ⥤ Over X`. -/ diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean index f736548..609ffd6 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean @@ -28,7 +28,7 @@ variable {C : Type u₁} [Category.{v₁} C] attribute [local instance] hasBinaryProducts_of_hasTerminal_and_pullbacks attribute [local instance] hasFiniteProducts_of_has_binary_and_terminal -attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts section @@ -69,11 +69,11 @@ end variable [HasTerminal C] [HasPullbacks C] -variable (I : C) [Exponentiable I] +variable (I : C) [Closed I] /-- The first leg of a cospan constructing a pullback diagram in `C` used to define `sections` . -/ def curryId : ⊤_ C ⟶ (I ⟹ I) := - CartesianClosed.curry (fst I (⊤_ C)) + MonoidalClosed.curry (fst I (⊤_ C)) variable {I} @@ -90,14 +90,14 @@ pullback diagram: ⊤_ C ----> I ⟹ I ```-/ abbrev sectionsObj (X : Over I) : C := - Limits.pullback (curryId I) ((exp I).map X.hom) + Limits.pullback (curryId I) ((ihom I).map X.hom) /-- The functoriality of `sectionsObj`. -/ def sectionsMap {X X' : Over I} (u : X ⟶ X') : sectionsObj X ⟶ sectionsObj X' := by fapply pullback.map · exact 𝟙 _ - · exact (exp I).map u.left + · exact (ihom I).map u.left · exact 𝟙 _ · simp only [comp_id, id_comp] · simp only [comp_id, ← Functor.map_comp, w] @@ -130,29 +130,30 @@ variable {I} in `C`. See `sectionsCurry`. -/ def sectionsCurryAux {X : Over I} {A : C} (u : (star I).obj A ⟶ X) : A ⟶ (I ⟹ X.left) := - CartesianClosed.curry (u.left) + MonoidalClosed.curry (u.left) /-- The currying operation `Hom ((star I).obj A) X → Hom A (I ⟹ X.left)`. -/ def sectionsCurry {X : Over I} {A : C} (u : (star I).obj A ⟶ X) : A ⟶ (sections I).obj X := by apply pullback.lift (terminal.from A) - (CartesianClosed.curry ((prodIsoTensorObj _ _).inv ≫ u.left)) (uncurry_injective _) - rw [uncurry_natural_left] - simp [curryId, uncurry_natural_right, uncurry_curry] + (MonoidalClosed.curry ((prodIsoTensorObj _ _).inv ≫ u.left)) + (MonoidalClosed.uncurry_injective _) + rw [MonoidalClosed.uncurry_natural_left] + simp [curryId, MonoidalClosed.uncurry_natural_right, MonoidalClosed.uncurry_curry] /-- The uncurrying operation `Hom A (section X) → Hom ((star I).obj A) X`. -/ def sectionsUncurry {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) : (star I).obj A ⟶ X := by let v₂ : A ⟶ (I ⟹ X.left) := v ≫ pullback.snd .. - have w : terminal.from A ≫ (curryId I) = v₂ ≫ (exp I).map X.hom := by + have w : terminal.from A ≫ (curryId I) = v₂ ≫ (ihom I).map X.hom := by rw [IsTerminal.hom_ext terminalIsTerminal (terminal.from A ) (v ≫ (pullback.fst ..))] simp [v₂, pullback.condition] dsimp [curryId] at w have w' := homEquiv_naturality_right_square (F := MonoidalCategory.tensorLeft I) - (adj := exp.adjunction I) _ _ _ _ w - simp [CartesianClosed.curry] at w' - refine Over.homMk ((prodIsoTensorObj I A).hom ≫ CartesianClosed.uncurry v₂) ?_ - · dsimp [CartesianClosed.uncurry] at * + (adj := ihom.adjunction I) _ _ _ _ w + simp [MonoidalClosed.curry] at w' + refine Over.homMk ((prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry v₂) ?_ + · dsimp [MonoidalClosed.uncurry] at * rw [Category.assoc, ← w'] simp [star_obj_hom] @@ -188,13 +189,13 @@ def coreHomEquiv : CoreHomEquiv (star I) (sections I) where simp only [star_map] rw [← Over.homMk_comp] -- note: in a newer version of mathlib this is `Over.homMk_eta` congr 1 - simp [CartesianClosed.uncurry_natural_left] + simp [MonoidalClosed.uncurry_natural_left] homEquiv_naturality_right := by intro A X' X u g dsimp [sectionsCurry, sectionsUncurry, curryId] apply pullback.hom_ext (IsTerminal.hom_ext terminalIsTerminal _ _) simp [sectionsMap, curryId] - rw [← CartesianClosed.curry_natural_right, Category.assoc] + rw [← MonoidalClosed.curry_natural_right, Category.assoc] variable (I) diff --git a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean similarity index 93% rename from Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean rename to Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean index 29faccd..e76ce64 100644 --- a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean +++ b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic import Poly.ForMathlib.CategoryTheory.CommSq namespace CategoryTheory.Functor diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean index 2111115..c1726dd 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean @@ -67,7 +67,7 @@ open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits F variable {C : Type u} [Category.{v} C] -attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts /-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I` has a right adjoint. -/ @@ -179,7 +179,7 @@ instance isMultiplicative : (ExponentiableMorphism (C:= C)).IsMultiplicative whe /-- A morphism with a pushforward is an exponentiable object in the slice category. -/ def exponentiableOverMk [HasFiniteWidePullbacks C] {X I : C} (f : X ⟶ I) [ExponentiableMorphism f] : - Exponentiable (Over.mk f) where + Closed (Over.mk f) where rightAdj := pullback f ⋙ pushforward f adj := by apply ofNatIsoLeft _ _ @@ -192,7 +192,7 @@ morphism `X.hom`. Here the pushforward functor along a morphism `f : I ⟶ J` is defined using the section functor `Over (Over.mk f) ⥤ Over J`. -/ -def ofOverExponentiable [HasFiniteWidePullbacks C] {I : C} (X : Over I) [Exponentiable X] : +def ofOverExponentiable [HasFiniteWidePullbacks C] {I : C} (X : Over I) [Closed X] : ExponentiableMorphism X.hom := ⟨X.iteratedSliceEquiv.inverse ⋙ sections X, ⟨by refine ofNatIsoLeft (Adjunction.comp ?_ ?_) (starIteratedSliceForwardIsoPullback X.hom) @@ -217,7 +217,7 @@ variable {C} [HasFiniteWidePullbacks C] [HasPushforwards C] /-- In a category where pushforwards exists along all morphisms, every slice category `Over I` is cartesian closed. -/ instance cartesianClosedOver (I : C) : - CartesianClosed (Over I) where + MonoidalClosed (Over I) where closed X := @exponentiableOverMk _ _ _ _ _ _ X.hom (HasPushforwards.exponentiable X.hom) end HasPushforwards @@ -226,13 +226,13 @@ namespace CartesianClosedOver open Over Reindex IsIso CartesianClosed HasPushforwards ExponentiableMorphism -variable {C} [HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)] +variable {C} [HasFiniteWidePullbacks C] {I J : C} [MonoidalClosed (Over J)] instance (f : I ⟶ J) : ExponentiableMorphism f := ExponentiableMorphism.ofOverExponentiable (Over.mk f) /-- A category with cartesian closed slices has pushforwards along all morphisms. -/ -instance hasPushforwards [Π (I : C), CartesianClosed (Over I)] : HasPushforwards C where +instance hasPushforwards [Π (I : C), MonoidalClosed (Over I)] : HasPushforwards C where exponentiable f := ExponentiableMorphism.ofOverExponentiable (Over.mk f) end CartesianClosedOver @@ -242,7 +242,7 @@ is exponentiable and all the slices are cartesian closed. -/ class LocallyCartesianClosed [HasFiniteWidePullbacks C] extends HasPushforwards C where /-- every slice category `Over I` is cartesian closed. This is filled in by default. -/ - cartesianClosedOver : Π (I : C), CartesianClosed (Over I) := HasPushforwards.cartesianClosedOver + cartesianClosedOver : Π (I : C), MonoidalClosed (Over I) := HasPushforwards.cartesianClosedOver namespace LocallyCartesianClosed @@ -256,7 +256,7 @@ attribute [scoped instance] hasFiniteLimits_of_hasTerminal_and_pullbacks instance mkOfHasPushforwards [HasPushforwards C] : LocallyCartesianClosed C where /-- A category with cartesian closed slices is locally cartesian closed. -/ -instance mkOfCartesianClosedOver [Π (I : C), CartesianClosed (Over I)] : +instance mkOfCartesianClosedOver [Π (I : C), MonoidalClosed (Over I)] : LocallyCartesianClosed C where variable [LocallyCartesianClosed C] @@ -282,8 +282,8 @@ abbrev ev' {I : C} (X : Over I) (Y : Over X.left) : Reindex X (Pi X Y) ⟶ Y := adj X.hom |>.counit.app Y /-- A locally cartesian closed category with a terminal object is cartesian closed. -/ -def cartesianClosed [HasTerminal C] : - CartesianClosed C := cartesianClosedOfEquiv <| equivOverTerminal C +def monoidalClosed [HasTerminal C] : + MonoidalClosed C := cartesianClosedOfEquiv <| equivOverTerminal C /-- The slices of a locally cartesian closed category are locally cartesian closed. -/ def overLocallyCartesianClosed (I : C) : LocallyCartesianClosed (Over I) := by @@ -291,6 +291,7 @@ def overLocallyCartesianClosed (I : C) : LocallyCartesianClosed (Over I) := by intro X exact cartesianClosedOfEquiv (C := Over (X.left)) X.iteratedSliceEquiv.symm +open CartesianClosed in /-- The exponential `X^^A` in the slice category `Over I` is isomorphic to the pushforward of the pullback of `X` along `A`. -/ def expIso {I : C} (A X : Over I) : Pi A (Reindex A X) ≅ A ⟹ X := Iso.refl _ diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean index fe6cdee..ff77bff 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sina Hazratpour, Emily Riehl -/ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic /-! # Beck-Chevalley natural transformations and natural isomorphisms diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean index a967405..5e92585 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean @@ -22,10 +22,10 @@ abbrev Psh (C : Type u) [Category.{v} C] : Type (max u (v + 1)) := Cᵒᵖ ⥤ T variable {C : Type*} [SmallCategory C] [HasTerminal C] -attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts -instance cartesianClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) : - CartesianClosed (Over P) := +instance monoidalClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) : + MonoidalClosed (Over P) := cartesianClosedOfEquiv (overEquivPresheafCostructuredArrow P).symm instance locallyCartesianClosed : LocallyCartesianClosed (Psh C) := by diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean index 6fd36bb..fea7cc5 100644 --- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean +++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean @@ -6,7 +6,7 @@ Authors: Sina Hazratpour import Mathlib.CategoryTheory.NatTrans import Mathlib.CategoryTheory.Functor.TwoSquare -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic open CategoryTheory Limits IsPullback diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean index d37c6a3..e33d783 100644 --- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean +++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Sina Hazratpour. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sina Hazratpour -/ -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic import Mathlib.CategoryTheory.Comma.Over.Pullback import Poly.ForMathlib.CategoryTheory.Comma.Over.Pullback import Mathlib.CategoryTheory.Monoidal.Closed.Cartesian @@ -100,6 +100,8 @@ structure Fan.Hom (c c' : Fan s X) where attribute [reassoc (attr := simp)] Fan.Hom.w_left Fan.Hom.w_right +-- TODO: this is taking ages to check since 4.28.0-rc1. +set_option maxHeartbeats 0 in @[simps] instance : Category (Fan s X) where Hom := Fan.Hom diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean index 988caad..0bb4cbe 100644 --- a/Poly/Type/Univariate.lean +++ b/Poly/Type/Univariate.lean @@ -189,7 +189,7 @@ def Obj.iget [DecidableEq P.B] {X} [Inhabited X] (x : P X) (i : P.Total) : X := @[simp] theorem iget_map [DecidableEq P.B] [Inhabited X] [Inhabited Y] (x : P X) (f : X → Y) (i : P.Total) (h : i.1 = x.1) : (P.map f x).iget i = f (x.iget i) := by - simp only [Obj.iget, fst_map, *, dif_pos, eq_self_iff_true] + simp only [Obj.iget, fst_map, *, dif_pos] cases x rfl diff --git a/lake-manifest.json b/lake-manifest.json index fe87d44..f32e2f9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "dd5e5d97469dec395f29661366030566355ad9be", + "rev": "b8dad038b1b3a05b77d6884b15b8db03ec01dca1", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", + "rev": "7311586e1a56af887b1081d05e80c11b6c41d212", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", + "rev": "b5908dbac486279f1133cb937648c63c30b455af", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.84", + "inputRev": "v0.0.86", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", + "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", + "rev": "23324752757bf28124a518ec284044c8db79fee5", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dff865b7ee7011518d59abfc101c368293173150", + "rev": "100083c18750b6a9b7553c65f6b052c0a2f6bcb4", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", + "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "v4.28.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "Poly", diff --git a/lean-toolchain b/lean-toolchain index fb18a7f..3e9b4e1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 \ No newline at end of file +leanprover/lean4:v4.28.0-rc1 \ No newline at end of file