diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean
index 3ca5ab0..17503a9 100644
--- a/Poly/Bifunctor/Basic.lean
+++ b/Poly/Bifunctor/Basic.lean
@@ -27,15 +27,13 @@ scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂
 @[simp]
 theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟'']
     (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
-    (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by
-  rfl
+    (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := rfl
 
 /-- Composition with `F,G` ordered like the arguments of `P` is considered `simp`ler. -/
 @[simp]
 theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
     (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
-    G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by
-  rfl
+    G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := rfl
 
 @[simps!]
 def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ}
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
index 4a8ab7b..0abbddf 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
@@ -17,8 +17,7 @@ variable {T : Type u₁} [Category.{v₁} T]
 namespace Over
 
 @[simp]
-theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := by
-  rfl
+theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := rfl
 
 /-- A variant of `homMk_comp` that can trigger in `simp`. -/
 @[simp]
@@ -30,8 +29,7 @@ lemma homMk_comp' {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_c
 @[simp]
 lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) :
     homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp =
-    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := by
-  rfl
+    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := rfl
 
 @[simp]
 lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) :=
@@ -57,8 +55,7 @@ lemma map_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
     ((Over.map Y.hom).map g).left = g.left := Over.map_map_left
 
 lemma map_homMk_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
-    map g = (Over.homMk g.left : Sigma Y Z ⟶ Sigma Y Z') := by
-  rfl
+    map g = (Over.homMk g.left : Sigma Y Z ⟶ Sigma Y Z') := rfl
 
 /-- The first projection of the sigma object. -/
 @[simps!]
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
index 61c042e..c772233 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour
 -/
 import Mathlib.CategoryTheory.Comma.Over.Pullback
-import Mathlib.CategoryTheory.ChosenFiniteProducts
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
 import Mathlib.CategoryTheory.Monad.Products
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
@@ -16,7 +16,9 @@ universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
-open Category Limits Comonad MonoidalCategory
+open Category Limits Comonad MonoidalCategory CartesianMonoidalCategory
+
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 variable {C : Type u₁} [Category.{v₁} C]
 
@@ -32,8 +34,7 @@ namespace Reindex
 variable [HasPullbacks C] {X : C}
 
 lemma hom {Y : Over X} {Z : Over X} :
-    (Reindex Y Z).hom = pullback.snd Z.hom Y.hom := by
-  rfl
+    (Reindex Y Z).hom = pullback.snd Z.hom Y.hom := rfl
 
 /-- `Reindex` is symmetric in its first and second arguments up to an isomorphism. -/
 def symmetryObjIso (Y Z : Over X) :
@@ -57,7 +58,7 @@ lemma symmetry_hom {Y Z : Over X} :
 def fstProj (Y Z : Over X) : Sigma Y (Reindex Y Z) ⟶ Y :=
   Over.homMk (pullback.snd Z.hom Y.hom) (by simp)
 
-lemma fstProj_sigma_fst (Y Z : Over X) : fstProj Y Z = Sigma.fst (Reindex Y Z) := by rfl
+lemma fstProj_sigma_fst (Y Z : Over X) : fstProj Y Z = Sigma.fst (Reindex Y Z) := rfl
 
 /-- The second projection out of the reindexed sigma object. -/
 def sndProj (Y Z : Over X) : Sigma Y (Reindex Y Z) ⟶ Z :=
@@ -87,7 +88,7 @@ end Reindex
 
 section BinaryProduct
 
-open ChosenFiniteProducts Sigma Reindex
+open Sigma Reindex
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -106,8 +107,6 @@ def isBinaryProductSigmaReindex (Y Z : Over X) :
     · exact congr_arg CommaMorphism.left (h ⟨ .right⟩)
     · exact congr_arg CommaMorphism.left (h ⟨ .left ⟩)
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-
 /-- The object `(Sigma Y) (Reindex Y Z)` is isomorphic to the binary product `Y × Z`
 in `Over X`. -/
 @[simps!]
@@ -122,12 +121,12 @@ def sigmaReindexIsoProdMk {Y : C} (f : Y ⟶ X) (Z : Over X) :
   sigmaReindexIsoProd (Over.mk f) _
 
 lemma sigmaReindexIsoProd_hom_comp_fst {Y Z : Over X} :
-    (sigmaReindexIsoProd Y Z).hom ≫ (fst Y Z) = (π_ Y Z) :=
+    (sigmaReindexIsoProd Y Z).hom ≫ fst Y Z = (π_ Y Z) :=
   IsLimit.conePointUniqueUpToIso_hom_comp
     (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.left⟩
 
 lemma sigmaReindexIsoProd_hom_comp_snd {Y Z : Over X} :
-    (sigmaReindexIsoProd Y Z).hom ≫ (snd Y Z) = (μ_ Y Z) :=
+    (sigmaReindexIsoProd Y Z).hom ≫ snd Y Z = (μ_ Y Z) :=
   IsLimit.conePointUniqueUpToIso_hom_comp
     (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.right⟩
 
@@ -137,10 +136,7 @@ end Over
 
 section TensorLeft
 
-open MonoidalCategory Over Functor ChosenFiniteProducts
-
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+open Over Functor
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -150,16 +146,16 @@ def Over.sigmaReindexNatIsoTensorLeft (Y : Over X) :
     (pullback Y.hom) ⋙ (map Y.hom) ≅ tensorLeft Y := by
   fapply NatIso.ofComponents
   · intro Z
-    simp only [const_obj_obj, Functor.id_obj, comp_obj, tensorLeft_obj, tensorObj, Over.pullback]
+    simp only [const_obj_obj, Functor.id_obj, comp_obj, Over.pullback]
     exact sigmaReindexIsoProd Y Z
   · intro Z Z' f
-    simp
+    dsimp
     ext1 <;> simp_rw [assoc]
-    · simp_rw [whiskerLeft_fst]
+    · rw [whiskerLeft_fst]
       iterate rw [sigmaReindexIsoProd_hom_comp_fst]
       ext
       simp
-    · simp_rw [whiskerLeft_snd]
+    · rw [whiskerLeft_snd]
       iterate rw [sigmaReindexIsoProd_hom_comp_snd, ← assoc, sigmaReindexIsoProd_hom_comp_snd]
       ext
       simp [Reindex.sndProj]
@@ -187,7 +183,7 @@ def equivOverTerminal [HasTerminal C] : Over (⊤_ C) ≌ C :=
 
 namespace Over
 
-open MonoidalCategory
+open CartesianMonoidalCategory
 
 variable {C}
 
@@ -201,15 +197,14 @@ 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] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 lemma whiskerLeftProdMapId [HasFiniteLimits C] {X : C} {A A' : C} {g : A ⟶ A'} :
     X ◁ g = prod.map (𝟙 X) g := by
   ext
-  · simp only [ChosenFiniteProducts.whiskerLeft_fst]
+  · simp only [whiskerLeft_fst]
     exact (Category.comp_id _).symm.trans (prod.map_fst (𝟙 X) g).symm
-  · simp only [ChosenFiniteProducts.whiskerLeft_snd]
+  · simp only [whiskerLeft_snd]
     exact (prod.map_snd (𝟙 X) g).symm
 
 def starForgetIsoTensorLeft [HasFiniteLimits C] (X : C) :
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
index 752a72c..e131353 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
@@ -21,14 +21,13 @@ universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
-open Category Limits MonoidalCategory CartesianClosed Adjunction Over
+open Category Limits MonoidalCategory CartesianMonoidalCategory CartesianClosed Adjunction Over
 
 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] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 section
 
@@ -36,34 +35,34 @@ variable [HasFiniteProducts C]
 
 /-- The isomorphism between `X ⨯ Y` and `X ⊗ Y` for objects `X` and `Y` in `C`.
 This is tautological by the definition of the cartesian monoidal structure on `C`.
-This isomorphism provides an interface between `prod.fst` and `ChosenFiniteProducts.fst`
+This isomorphism provides an interface between `prod.fst` and `CartesianMonoidalCategory.fst`
 as well as between `prod.map` and `tensorHom`. -/
 def prodIsoTensorObj (X Y : C) : X ⨯ Y ≅ X ⊗ Y := Iso.refl _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_inv_fst {X Y : C} :
-    (prodIsoTensorObj X Y).inv ≫ prod.fst = ChosenFiniteProducts.fst X Y :=
+    (prodIsoTensorObj X Y).inv ≫ prod.fst = fst X Y :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_inv_snd {X Y : C} :
-    (prodIsoTensorObj X Y).inv ≫ prod.snd = ChosenFiniteProducts.snd X Y :=
+    (prodIsoTensorObj X Y).inv ≫ prod.snd = snd X Y :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_hom_fst {X Y : C} :
-    (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.fst X Y = prod.fst :=
+    (prodIsoTensorObj X Y).hom ≫ fst X Y = prod.fst :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_hom_snd {X Y : C} :
-    (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.snd X Y = prod.snd :=
+    (prodIsoTensorObj X Y).hom ≫ snd X Y = prod.snd :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodMap_comp_prodIsoTensorObj_hom {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) :
-    prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ g) := by
-  apply ChosenFiniteProducts.hom_ext <;> simp
+    prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ₘ g) := by
+  apply hom_ext <;> simp
 
 end
 
@@ -73,7 +72,7 @@ variable (I : C) [Exponentiable I]
 
 /-- The first leg of a cospan constructing a pullback diagram in `C` used to define `sections` . -/
 def curryId : ⊤_ C ⟶ (I ⟹ I) :=
-  CartesianClosed.curry (ChosenFiniteProducts.fst I (⊤_ C))
+  CartesianClosed.curry (fst I (⊤_ C))
 
 variable {I}
 
diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean
index ab84dd6..98eee42 100644
--- a/Poly/ForMathlib/CategoryTheory/Elements.lean
+++ b/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 (by rfl)) := by
+    G.map (Subtype.mk (α := Y ⟶ Z) 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)⟩
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean
index e26775e..2111115 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean
@@ -62,11 +62,12 @@ universe v u
 
 namespace CategoryTheory
 
-open CategoryTheory Category MonoidalCategory Limits Functor Adjunction Over
+open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits Functor Adjunction
+  Over
 
 variable {C : Type u} [Category.{v} C]
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 /-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I`
 has a right adjoint. -/
@@ -223,7 +224,7 @@ end HasPushforwards
 
 namespace CartesianClosedOver
 
-open Over Reindex IsIso ChosenFiniteProducts CartesianClosed HasPushforwards ExponentiableMorphism
+open Over Reindex IsIso CartesianClosed HasPushforwards ExponentiableMorphism
 
 variable {C} [HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)]
 
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
index d2b7952..eca421e 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
@@ -129,8 +129,6 @@ def paste : cartesian (pasteCell f u) := by
   · unfold pasteCell2
     apply cartesian.whiskerRight (cellLeftCartesian f u)
 
-#check pushforwardPullbackTwoSquare
-
 -- use `pushforwardPullbackTwoSquare` to construct this iso.
 def pentagonIso : map u ⋙ pushforward f ≅
   pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) := by
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean
index 065ad49..2fad239 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean
@@ -22,7 +22,7 @@ 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] ChosenFiniteProducts.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 instance cartesianClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) :
     CartesianClosed (Over P) :=
diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean
index 6eb67a0..cd1f798 100644
--- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean
+++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean
@@ -18,6 +18,8 @@ variable {K : Type*} [Category K] {D : Type*} [Category D]
 
 namespace NatTrans
 
+open Functor
+
 /-- A natural transformation is cartesian if every commutative square of the following form is
 a pullback.
 ```
diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
index 7362e40..0a152d2 100644
--- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
+++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
@@ -53,8 +53,7 @@ structure Fan where
   snd : pullback fst s ⟶ X
 
 theorem Fan.fst_mk {pt : C} (f : pt ⟶ B) (g : pullback f s ⟶ X) :
-    Fan.fst (Fan.mk f g) = f := by
-  rfl
+    Fan.fst (Fan.mk f g) = f := rfl
 
 variable {s X}
 
@@ -84,8 +83,7 @@ def pullbackMap {c' c : Fan s X} (f : c'.pt ⟶ c.pt)
   ((Over.pullback s).map (Over.homMk f (by aesop) : Over.mk (c'.fst) ⟶ Over.mk c.fst)).left
 
 theorem pullbackMap_comparison {P} {c : Fan s X} (f : P ⟶ c.pt) :
-    pullbackMap (c' := Fan.mk (f ≫ c.fst) (comparison f ≫ c.snd)) (c := c) f = comparison f := by
-  rfl
+    pullbackMap (c' := Fan.mk (f ≫ c.fst) (comparison f ≫ c.snd)) (c := c) f = comparison f := rfl
 
 /-- A map to the apex of a partial product cone induces a partial product cone by precomposition. -/
 @[simps]
diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean
index 77abc99..a684339 100644
--- a/Poly/UvPoly/Basic.lean
+++ b/Poly/UvPoly/Basic.lean
@@ -223,10 +223,10 @@ instance : Category (UvPoly.Total C) where
   id P := UvPoly.Hom.id P.poly
   comp := UvPoly.Hom.comp
   id_comp := by
-    simp [UvPoly.Hom.id, UvPoly.Hom.comp]
+    simp [UvPoly.Hom.comp]
     sorry
   comp_id := by
-    simp [UvPoly.Hom.id, UvPoly.Hom.comp]
+    simp [UvPoly.Hom.comp]
     sorry
   assoc := by
     simp [UvPoly.Hom.comp]
@@ -323,8 +323,7 @@ def proj {Γ X : C} (P : UvPoly E B) (f : Γ ⟶ P @ X) :
 
 @[simp]
 theorem proj_fst {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} :
-    (proj P f).fst = f ≫ P.fstProj X := by
-  rfl
+    (proj P f).fst = f ≫ P.fstProj X := rfl
 
 /-- The second component of `proj` is a comparison map of pullbacks composed with `ε P X ≫ prod.snd` -/
 -- formerly `polyPair_snd_eq_comp_u₂'`
diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean
index 7e000fe..4ccc736 100644
--- a/Poly/UvPoly/UPFan.lean
+++ b/Poly/UvPoly/UPFan.lean
@@ -23,8 +23,7 @@ def equiv (P : UvPoly E B) (Γ : C) (X : C) :
     dsimp
     symm
     fapply partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩
-    · simp [partialProd.lift]
-      rfl
+    · simp; rfl
     · sorry
   right_inv := by
     intro ⟨b, e⟩
diff --git a/Poly/deprecated/Exponentiable.lean b/Poly/deprecated/Exponentiable.lean
index 9bfb215..19250cc 100644
--- a/Poly/deprecated/Exponentiable.lean
+++ b/Poly/deprecated/Exponentiable.lean
@@ -84,18 +84,15 @@ example (I J X : C) (f : J ⟶ I) (p : X ⟶ I) :
 
 /-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is `pullback.snd`. -/
 lemma hom_eq_pullback_snd {I J : C} (f : J ⟶ I) (X : Over I):
-    ((Δ_ f).obj X).hom = pullback.snd := by
-  rfl
+    ((Δ_ f).obj X).hom = pullback.snd := rfl
 
 example {I : C} (f : J ⟶ I) (p : X ⟶ I) :
-    ((Δ_ f).obj (Over.mk p)).hom = pullback.snd := by
-  rfl
+    ((Δ_ f).obj (Over.mk p)).hom = pullback.snd := rfl
 
 /-- For objects `X` and `Y` in `Over I`, the base-change of `X` along `Y.hom` is
 equal to `pullback.snd : pullback X.hom Y.hom ⟶ Y.left` -/
 example {I : C} (X Y : Over I) :
-    ((Δ_ Y.hom).obj X).hom = pullback.snd := by
-  rfl
+    ((Δ_ Y.hom).obj X).hom = pullback.snd := rfl
 
 -- /-- The base-change of `Y` along `X` is `pullback.snd (f:= Y.hom) (g:= X.hom)` -/
 -- lemma hom_eq_pullback_snd' [HasPullbacks C] {I : C} (X Y : Over I) :
diff --git a/Poly/deprecated/ForMathlib.lean b/Poly/deprecated/ForMathlib.lean
index 145101d..2d4ad53 100644
--- a/Poly/deprecated/ForMathlib.lean
+++ b/Poly/deprecated/ForMathlib.lean
@@ -23,8 +23,7 @@ lemma homMk_comp {B : C} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left 
 
 @[simp]
 lemma left_homMk {B : C} {U V : Over B} (f : U ⟶ V) (h) :
-    homMk f.left h = f := by
-  rfl
+    homMk f.left h = f := rfl
 
 end CategoryTheory.Over
 
@@ -42,12 +41,10 @@ variable {C : Type*} [Category C] [HasFiniteProducts C]
 attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
 
 @[simp]
-theorem ofFiniteProducts_fst (X Y : C) : fst X Y = prod.fst := by
-  rfl
+theorem ofFiniteProducts_fst (X Y : C) : fst X Y = prod.fst := rfl
 
 @[simp]
-theorem ofFiniteProducts_snd  (X Y : C) : snd X Y = prod.snd := by
-  rfl
+theorem ofFiniteProducts_snd  (X Y : C) : snd X Y = prod.snd := rfl
 
 @[simp]
 theorem ofFiniteProducts_whiskerLeft {Y Z : C} (X : C) (f : Y ⟶ Z) :
diff --git a/Poly/deprecated/PartialProduct.lean b/Poly/deprecated/PartialProduct.lean
index 053296e..3fc1449 100644
--- a/Poly/deprecated/PartialProduct.lean
+++ b/Poly/deprecated/PartialProduct.lean
@@ -53,8 +53,7 @@ structure Fan where
   snd : pullback fst s ⟶ X
 
 theorem Fan.fst_mk {pt : C} (f : pt ⟶ B) (g : pullback f s ⟶ X) :
-    Fan.fst (Fan.mk f g) = f := by
-  rfl
+    Fan.fst (Fan.mk f g) = f := rfl
 
 variable {s X}
 
@@ -84,8 +83,7 @@ def pullbackMap {c' c : Fan s X} (f : c'.pt ⟶ c.pt)
   ((Over.pullback s).map (Over.homMk f (by aesop) : Over.mk (c'.fst) ⟶ Over.mk c.fst)).left
 
 theorem pullbackMap_comparison {P} {c : Fan s X} (f : P ⟶ c.pt) :
-    pullbackMap (c' := Fan.mk (f ≫ c.fst) (comparison f ≫ c.snd)) (c := c) f = comparison f := by
-  rfl
+    pullbackMap (c' := Fan.mk (f ≫ c.fst) (comparison f ≫ c.snd)) (c := c) f = comparison f := rfl
 
 /-- A map to the apex of a partial product cone induces a partial product cone by precomposition. -/
 @[simps]
diff --git a/lake-manifest.json b/lake-manifest.json
index d16603f..a84145e 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": "b3fb998509f92a040e362f8a06f8ee2825ec8c10",
-   "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": "75d7aea6c81efeb68701164edaaa9116f06b91ba",
+   "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b6b76a5d7cc1c8b11c52f12a7bd90c460b7cba5a",
+   "rev": "7279fc299b10681b00aefe1edd0668766cead87c",
    "name": "seq",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,57 +25,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fbe595fc740ee7a1789c6e6ebefa322e054a41c0",
+   "rev": "0faf9c7e5dce691f1a9e2e5dc1aa2499e9acb2e0",
    "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": "dd423cf2b153b5b14cb017ee4beae788565a3925",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/jcommelin/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "458e2d3feda3999490987eabee57b8bb88b1949c",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "bump_to_v4.18.0-rc1",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "c07de335d35ed6b118e084ec48cffc39b40d29d2",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb",
-   "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": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
+   "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba020ed434b9c5877eb62ff072a28f5ec56eb871",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c",
+   "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
+   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.53",
+   "inputRev": "v0.0.67",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
+   "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
+   "rev": "867d9dc77534341321179c9aa40fceda675c50d4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -145,11 +95,21 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f2fb9809751c4646c68c329b14f7d229a93176fd",
+   "rev": "3cabaef23886b82ba46f07018f2786d9496477d6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 2e9f658..e4e5822 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-package «Poly» where
+package Poly where
   -- Settings applied to both builds and interactive editing
   leanOptions := #[
     ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
@@ -14,11 +14,11 @@ require mathlib from git
 require seq from git "https://github.com/Vtec234/lean4-seq"
 
 @[default_target]
-lean_lib «Poly» where
+lean_lib Poly where
   -- add any library configuration options here
 
 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" @ "main"
\ No newline at end of file
+  "https://github.com/leanprover/doc-gen4" @ "v4.22.0-rc3"
diff --git a/lean-toolchain b/lean-toolchain
index ee45541..28f76d1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.18.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.22.0-rc3
\ No newline at end of file