From 4e69398cf4cfcad9d0965b3dc5a8751fea0d396a Mon Sep 17 00:00:00 2001
From: shiv <33400784+sosudo@users.noreply.github.com>
Date: Mon, 9 Nov 2026 02:10:13 -0500
Subject: [PATCH] chore: bump Poly to Lean 4.34.1

Update Lean, mathlib, and doc-gen4 to 4.34.1. Include the API fixes needed to build with this toolchain and vendor checkdecls, which has no matching upstream release. Correct the README version and documentation links.

This is the compatibility portion of #41. The proof additions are separate. The only indentation-only change is needed for a continued variable declaration to parse.

Compatibility note: `UvPoly.comp`, `UvPoly.compFunctorIso`, and `UvPoly.monoidal` drop duplicate instance arguments; their section assumptions remain.
---
 .gitignore                                    |   1 +
 Poly/Bifunctor/Basic.lean                     |  19 +-
 Poly/Bifunctor/Sigma.lean                     |  96 ++++++---
 .../CategoryTheory/Comma/Over/Pullback.lean   | 114 +++++++---
 .../CategoryTheory/Comma/Over/Sections.lean   |  87 ++++++--
 Poly/ForMathlib/CategoryTheory/Elements.lean  |  20 +-
 .../Shapes/Pullback/IsPullback/Basic.lean     |   8 +-
 .../LocallyCartesianClosed/Basic.lean         |   9 +-
 .../LocallyCartesianClosed/BeckChevalley.lean |  22 +-
 .../Distributivity.lean                       |  20 +-
 Poly/ForMathlib/CategoryTheory/NatTrans.lean  |   2 +-
 .../CategoryTheory/PartialProduct.lean        |  21 +-
 Poly/ForMathlib/CategoryTheory/Types.lean     |   8 +-
 Poly/MvPoly/Basic.lean                        |   2 +-
 Poly/Type/Univariate.lean                     |  12 +-
 Poly/UvPoly/Basic.lean                        |  41 ++--
 Poly/UvPoly/UPFan.lean                        |   2 +-
 Poly/UvPoly/UPIso.lean                        |  13 +-
 Poly/Widget/CommDiag.lean                     |  11 +-
 README.md                                     |  12 +-
 lake-manifest.json                            |  36 ++--
 lakefile.lean                                 |   6 +-
 lean-toolchain                                |   2 +-
 vendor/checkdecls/.gitignore                  |   4 +
 vendor/checkdecls/LICENSE                     | 201 ++++++++++++++++++
 vendor/checkdecls/Main.lean                   |  26 +++
 vendor/checkdecls/UPSTREAM.md                 |  25 +++
 vendor/checkdecls/lake-manifest.json          |   6 +
 vendor/checkdecls/lakefile.lean               |  13 ++
 vendor/checkdecls/lean-toolchain              |   1 +
 30 files changed, 641 insertions(+), 199 deletions(-)
 create mode 100644 vendor/checkdecls/.gitignore
 create mode 100644 vendor/checkdecls/LICENSE
 create mode 100644 vendor/checkdecls/Main.lean
 create mode 100644 vendor/checkdecls/UPSTREAM.md
 create mode 100644 vendor/checkdecls/lake-manifest.json
 create mode 100644 vendor/checkdecls/lakefile.lean
 create mode 100644 vendor/checkdecls/lean-toolchain

diff --git a/.gitignore b/.gitignore
index fa55280..79529d2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -40,6 +40,7 @@ docs/_includes/sorries.md
 *.synctex.gz(busy)
 *.pdfsync
 *.json
+!vendor/checkdecls/lake-manifest.json
 *.auctex-auto
 
 build/
diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean
index 17503a9..976ad57 100644
--- a/Poly/Bifunctor/Basic.lean
+++ b/Poly/Bifunctor/Basic.lean
@@ -39,8 +39,11 @@ theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
 def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ}
     (i : F₁ ≅ F₂) (j : P₁ ≅ P₂) : F₁ ⋙₂ P₁ ≅ F₂ ⋙₂ P₂ :=
   NatIso.ofComponents₂ (fun C D => (j.app C).app (F₁.obj D) ≪≫ (P₂.obj C).mapIso (i.app D))
-    (fun _ _ => by simp [NatTrans.naturality_app_assoc])
+    (fun _ _ => by
+      dsimp [comp₂]
+      simp [NatTrans.naturality_app_assoc])
     (fun C f => by
+      dsimp [comp₂]
       have := congr_arg (P₂.obj C).map (i.hom.naturality f)
       simp only [map_comp] at this
       simp [this])
@@ -70,12 +73,12 @@ theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟
     (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) :
     -- The `op`s really are a pain. Why can't they be definitional like in Lean 3 :(
     (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) := by
-  simp [← FunctorToTypes.naturality₂_left]
+  exact FunctorToTypes.naturality₂_left _ _ i f.op g
 
 theorem comp₂_naturality₂_right (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
     (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X : 𝒞) (Y Z : 𝒟) (f : X ⟶ F.obj Y) (g : Y ⟶ Z) :
     (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) := by
-  simp [← FunctorToTypes.naturality₂_right]
+  exact FunctorToTypes.naturality₂_right _ _ i g f
 
 end coyoneda
 
@@ -87,8 +90,14 @@ variable {𝒟 : Type*} [Category 𝒟]
 def coyoneda_iso {F : 𝒞 ⥤ 𝒟} {G : 𝒟 ⥤ 𝒞} (A : F ⊣ G) :
     F.op ⋙ coyoneda (C := 𝒟) ≅ G ⋙₂ coyoneda (C := 𝒞) :=
   NatIso.ofComponents₂ (fun C D => Equiv.toIso <| A.homEquiv C.unop D)
-    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_left])
-    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_right])
+    (fun _ f => by
+      apply ConcreteCategory.hom_ext
+      intro g
+      exact A.homEquiv_naturality_left f.unop g)
+    (fun _ f => by
+      apply ConcreteCategory.hom_ext
+      intro g
+      exact A.homEquiv_naturality_right g f)
 
 end Adjunction
 end CategoryTheory
diff --git a/Poly/Bifunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean
index d453d2d..70e372f 100644
--- a/Poly/Bifunctor/Sigma.lean
+++ b/Poly/Bifunctor/Sigma.lean
@@ -45,20 +45,22 @@ a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward.
 - known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/
 def Sigma {F : 𝒞 ⥤ Type w} (G : F.Elements ⥤ 𝒟 ⥤ Type v) : 𝒞 ⥤ 𝒟 ⥤ Type (max w v) := by
   refine curry.obj {
-    obj := fun (C, D) => (a : F.obj C) × (G.obj ⟨C, a⟩).obj D
-    map := fun (f, g) ⟨a, b⟩ =>
-      ⟨F.map f a, (G.map ⟨f, rfl⟩).app _ ((G.obj ⟨_, a⟩).map g b)⟩
+    obj := fun (C, D) => (a : F.obj C) × (G.obj (F.elementsMk C a)).obj D
+    map := fun fg => TypeCat.ofHom fun ⟨a, b⟩ =>
+      ⟨F.map fg.1 a, (G.map ⟨fg.1, rfl⟩).app _ ((G.obj (F.elementsMk _ a)).map fg.2 b)⟩
     map_id := ?_
     map_comp := ?_
   } <;> {
     intros
-    ext ⟨a, b⟩ : 1
-    dsimp
+    apply ConcreteCategory.hom_ext
+    rintro ⟨a, b⟩
+    dsimp +instances
     congr! 1 with h
     . simp
-    . rw! [h]; simp [FunctorToTypes.naturality]
+    . rw! [h]; simp [NatTrans.naturality_apply]
   }
 
+set_option backward.isDefEq.respectTransparency.types false in
 def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
     /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements`
     could `NatTrans.mapElements i.hom` generalize to?
@@ -69,38 +71,42 @@ def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
   refine NatIso.ofComponents₂
     (fun C D => Equiv.toIso {
       toFun := fun ⟨a, b⟩ => ⟨i.hom.app C a, b⟩
-      invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp) b⟩
-      left_inv := fun ⟨_, _⟩ => by simp
-      right_inv := fun ⟨_, _⟩ => by simp
+      invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp [NatTrans.mapElements]) b⟩
+      left_inv := fun ⟨_, _⟩ => by simp [Sigma, NatTrans.mapElements]
+      right_inv := fun ⟨_, _⟩ => by simp [Sigma]
     }) ?_ ?_ <;> {
       intros
-      ext : 1
-      dsimp
+      apply ConcreteCategory.hom_ext
+      rintro ⟨a, b⟩
+      dsimp +instances [Sigma, Equiv.toIso]
       apply have h := ?_; Sigma.ext h ?_
-      . simp [FunctorToTypes.naturality]
-      . dsimp [Sigma] at h ⊢
+      . simp [NatTrans.naturality_apply]
+      . dsimp +instances [Sigma] at h ⊢
         rw! [← h]
         simp [NatTrans.mapElements]
     }
 
+set_option backward.isDefEq.respectTransparency.types false in
 def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type v} (i : G₁ ≅ G₂) :
     Sigma G₁ ≅ Sigma G₂ := by
   refine NatIso.ofComponents₂
     (fun C D => Equiv.toIso {
-      toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app ⟨C, a⟩).app D b⟩
-      invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app ⟨C, a⟩).app D b⟩
-      left_inv := fun ⟨_, _⟩ => by simp
-      right_inv := fun ⟨_, _⟩ => by simp
+      toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app (F.elementsMk C a)).app D b⟩
+      invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app (F.elementsMk C a)).app D b⟩
+      left_inv := fun ⟨_, _⟩ => by simp [Sigma]
+      right_inv := fun ⟨_, _⟩ => by simp [Sigma]
     }) ?_ ?_ <;> {
       intros
-      ext : 1
-      dsimp
+      apply ConcreteCategory.hom_ext
+      rintro ⟨a, b⟩
+      dsimp +instances [Sigma, Equiv.toIso]
       apply have h := ?_; Sigma.ext h ?_
       . simp
-      . dsimp [Sigma] at h ⊢
-        simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right]
+      . dsimp +instances [Sigma] at h ⊢
+        simp [FunctorToTypes.naturality₂_left]
     }
 
+set_option backward.isDefEq.respectTransparency false in
 theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
     {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) :
     G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by
@@ -110,12 +116,15 @@ theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
     . intro; simp
     . intros
       apply heq_of_eq
-      ext : 1
-      apply Sigma.ext <;> simp
+      apply ConcreteCategory.hom_ext
+      intro x
+      apply Sigma.ext <;> simp [comp₂, Sigma]
   . intros
     apply heq_of_eq
-    ext : 3
-    apply Sigma.ext <;> simp
+    ext D : 2
+    apply ConcreteCategory.hom_ext
+    intro x
+    apply Sigma.ext <;> simp [comp₂, Sigma]
 
 end CategoryTheory.Functor
 
@@ -133,41 +142,60 @@ def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X 
   invFun p := p.snd.left
   left_inv _ := by simp
   right_inv := fun _ => by
-    dsimp; congr! 1 with h
+    dsimp +instances; congr! 1 with h
     . simp
     . rw! [h]; simp
 
 @[simps]
 def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ where
   functor := {
-    obj := fun x => .op <| Over.mk x.snd
-    map := fun f => .op <| Over.homMk f.val.unop (by simpa using f.property)
+    obj := fun x => .op <| Over.mk x.val
+    map := fun f => .op <| Over.homMk f.hom.unop (by simpa using f.map_val)
   }
   inverse := {
-    obj := fun U => ⟨.op U.unop.left, U.unop.hom⟩
+    obj := fun U => (yoneda.obj A).elementsMk (.op U.unop.left) U.unop.hom
     map := fun f => ⟨.op f.unop.left, by simp⟩
   }
-  unitIso := NatIso.ofComponents Iso.refl (by simp)
+  unitIso := NatIso.ofComponents Iso.refl (by intro X Y f; simp; rfl)
   counitIso := NatIso.ofComponents Iso.refl
     -- TODO: `simp` fails to unify `id_comp`/`comp_id`
     (fun f => by simp [Category.comp_id f, Category.id_comp f])
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- For `X ∈ 𝒞` and `f ∈ 𝒞/A`, `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)`. -/
 def forget_iso_Sigma (A : 𝒞) :
     Over.forget A ⋙₂ coyoneda (C := 𝒞) ≅
     Functor.Sigma ((equivalence_Elements A).functor ⋙ coyoneda (C := Over A)) := by
   refine NatIso.ofComponents₂ (fun X U => Equiv.toIso <| equiv_Sigma X.unop U) ?_ ?_
   . intros X Y U f
-    ext : 1
-    dsimp
+    apply ConcreteCategory.hom_ext
+    intro g
+    change X.unop ⟶ U.left at g
+    dsimp +instances [Functor.comp₂, Functor.Sigma]
+    simp only [Equiv.toIso_hom_hom_apply]
+    change (⟨(f.unop ≫ g) ≫ U.hom, Over.homMk (f.unop ≫ g) rfl⟩ :
+      (b : Y.unop ⟶ A) × (Over.mk b ⟶ U)) =
+      ⟨f.unop ≫ (g ≫ U.hom),
+        (Over.homMk f.unop rfl :
+          Over.mk (f.unop ≫ (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom)) ≫
+        Over.homMk g rfl ≫ 𝟙 U⟩
     apply have h := ?_; Sigma.ext h ?_
     . simp
     . dsimp at h ⊢
       rw! [h]
       simp
   . intros X Y U f
-    ext : 1
-    dsimp
+    apply ConcreteCategory.hom_ext
+    intro g
+    change U.unop ⟶ X.left at g
+    dsimp +instances [Functor.comp₂, Functor.Sigma]
+    simp only [Equiv.toIso_hom_hom_apply]
+    change (⟨(g ≫ f.left) ≫ Y.hom, Over.homMk (g ≫ f.left) rfl⟩ :
+      (b : U.unop ⟶ A) × (Over.mk b ⟶ Y)) =
+      ⟨𝟙 U.unop ≫ (g ≫ X.hom),
+        (Over.homMk (𝟙 U.unop) rfl :
+          Over.mk (𝟙 U.unop ≫ (g ≫ X.hom)) ⟶ Over.mk (g ≫ X.hom)) ≫
+        Over.homMk g rfl ≫ f⟩
     apply have h := ?_; Sigma.ext h ?_
     . simp
     . dsimp at h ⊢
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
index d5569d6..8ec5e03 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
@@ -32,9 +32,13 @@ theorem isCartesian_mapPullbackAdj_counit [HasPullbacks C] {X Y : C} (f : X ⟶
     (h₁₂ := Over.homMk (V := Over.mk f) (pullback.snd B.hom f) <| by simp)
     (v₁₃ := Over.mkIdTerminal.from _)
     (h₂₂ := Over.mkIdTerminal.from _)
-  case p => ext; simp
+  case p =>
+    ext
+    simp
+    exact pullback.lift_fst ..
   . apply (Over.forget Y).reflect_isPullback
     convert (IsPullback.of_hasPullback A.hom f).flip using 1 <;> simp
+    exact pullback.lift_snd ..
   . apply (Over.forget Y).reflect_isPullback
     convert (IsPullback.of_hasPullback B.hom f).flip using 1 <;> simp
 
@@ -102,7 +106,7 @@ end Reindex
 
 section BinaryProduct
 
-open Sigma Reindex
+open Over.Sigma Reindex
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -113,13 +117,21 @@ def isBinaryProductSigmaReindex (Y Z : Over X) :
   · intro s
     fapply Over.homMk
     · exact pullback.lift (s.π.app ⟨.right⟩).left (s.π.app ⟨ .left ⟩).left (by aesop)
-    · aesop
-  · rintro s ⟨⟨l⟩|⟨r⟩⟩ <;> apply Over.OverMorphism.ext <;> simp [Reindex.sndProj]
+    · change pullback.lift _ _ _ ≫ pullback.snd Z.hom Y.hom ≫ Y.hom = s.pt.hom
+      rw [pullback.lift_snd_assoc]
+      exact Over.w _
+  · rintro s ⟨⟨l⟩|⟨r⟩⟩ <;> apply Over.OverMorphism.ext
+    · exact pullback.lift_snd ..
+    · exact pullback.lift_fst ..
   · intro s m h
     apply Over.OverMorphism.ext
-    apply pullback.hom_ext <;> simp
-    · exact congr_arg CommaMorphism.left (h ⟨ .right⟩)
-    · exact congr_arg CommaMorphism.left (h ⟨ .left ⟩)
+    apply pullback.hom_ext
+    · change m.left ≫ pullback.fst Z.hom Y.hom = pullback.lift _ _ _ ≫ pullback.fst _ _
+      rw [pullback.lift_fst]
+      exact congr_arg CommaMorphism.left (h ⟨ .right⟩)
+    · change m.left ≫ pullback.snd Z.hom Y.hom = pullback.lift _ _ _ ≫ pullback.snd _ _
+      rw [pullback.lift_snd]
+      exact congr_arg CommaMorphism.left (h ⟨ .left ⟩)
 
 /-- The object `(Sigma Y) (Reindex Y Z)` is isomorphic to the binary product `Y × Z`
 in `Over X`. -/
@@ -150,7 +162,7 @@ end Over
 
 section TensorLeft
 
-open Over Functor
+open Over CategoryTheory.Functor
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -160,19 +172,32 @@ 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, Over.pullback]
     exact sigmaReindexIsoProd Y Z
   · intro Z Z' f
-    dsimp
-    ext1 <;> simp_rw [assoc]
-    · rw [whiskerLeft_fst]
-      iterate rw [sigmaReindexIsoProd_hom_comp_fst]
-      ext
+    have hm : Y ◁ f = Limits.prod.map (𝟙 Y) f := by
+      ext1
+      · simp only [whiskerLeft_fst]
+        exact (Category.comp_id _).symm.trans (Limits.prod.map_fst (𝟙 Y) f).symm
+      · simp only [whiskerLeft_snd]
+        exact (Limits.prod.map_snd (𝟙 Y) f).symm
+    change (map Y.hom).map ((pullback Y.hom).map f) ≫ (sigmaReindexIsoProd Y Z').hom =
+      (sigmaReindexIsoProd Y Z).hom ≫ Y ◁ f
+    rw [hm]
+    change (map Y.hom).map ((pullback Y.hom).map f) ≫ (sigmaReindexIsoProd Y Z').hom =
+      (sigmaReindexIsoProd Y Z).hom ≫ Limits.prod.map (𝟙 Y) f
+    have hf (Z : Over X) : (sigmaReindexIsoProd Y Z).hom ≫ Limits.prod.fst =
+        Reindex.fstProj Y Z := sigmaReindexIsoProd_hom_comp_fst
+    have hs (Z : Over X) : (sigmaReindexIsoProd Y Z).hom ≫ Limits.prod.snd =
+        Reindex.sndProj Y Z := sigmaReindexIsoProd_hom_comp_snd
+    apply Limits.prod.hom_ext
+    · simp only [assoc, hf, Limits.prod.map_fst, Category.comp_id]
+      apply Over.OverMorphism.ext
       simp
-    · rw [whiskerLeft_snd]
-      iterate rw [sigmaReindexIsoProd_hom_comp_snd, ← assoc, sigmaReindexIsoProd_hom_comp_snd]
-      ext
+      exact pullback.lift_snd ..
+    · rw [assoc, hs, assoc, Limits.prod.map_snd, ← assoc, hs]
+      apply Over.OverMorphism.ext
       simp [Reindex.sndProj]
+      exact pullback.lift_fst ..
 
 lemma Over.sigmaReindexNatIsoTensorLeft_hom_app
     {Y : Over X} (Z : Over X) :
@@ -192,8 +217,15 @@ def Functor.toOverTerminal [HasTerminal C] : C ⥤ Over (⊤_ C) where
 /-- The slice category over the terminal object is equivalent to the original category. -/
 def equivOverTerminal [HasTerminal C] : Over (⊤_ C) ≌ C :=
   CategoryTheory.Equivalence.mk (Over.forget _) (Functor.toOverTerminal C)
-    (NatIso.ofComponents (fun X => Over.isoMk (Iso.refl _)))
-    (NatIso.ofComponents (fun X => Iso.refl _))
+    (NatIso.ofComponents (fun X => Over.isoMk (Iso.refl _)) (by
+      intro X Y f
+      ext
+      change f.left ≫ 𝟙 _ = 𝟙 _ ≫ f.left
+      simp))
+    (NatIso.ofComponents (fun X => Iso.refl _) (by
+      intro X Y f
+      change f ≫ 𝟙 _ = 𝟙 _ ≫ f
+      simp))
 
 namespace Over
 
@@ -201,9 +233,17 @@ open CartesianMonoidalCategory
 
 variable {C}
 
+private theorem star_obj_hom_eq_fst [HasBinaryProducts C] (I X : C) :
+    ((star I).obj X).hom = prod.fst :=
+  prod.lift_fst ..
+
 lemma star_map [HasBinaryProducts C] {X : C} {Y Z : C} (f : Y ⟶ Z) :
-    (star X).map f = Over.homMk (prod.map (𝟙 X) f) (by aesop) := by
-  simp [star]
+    (star X).map f = Over.homMk (prod.map (𝟙 X) f) (by
+      change prod.map (𝟙 X) f ≫ ((star X).obj Z).hom = ((star X).obj Y).hom
+      rw [star_obj_hom_eq_fst, star_obj_hom_eq_fst]
+      exact (prod.map_fst _ _).trans (Category.comp_id _)) := by
+  apply Over.OverMorphism.ext
+  exact star_map_left X f
 
 /-- Note that the binary products assumption is necessary: the existence of a right adjoint to
 `Over.forget X` is equivalent to the existence of each binary product `X ⨯ -`.
@@ -227,7 +267,10 @@ def starForgetIsoTensorLeft [HasFiniteLimits C] (X : C) :
   · intro Z
     exact Iso.refl _
   · intro Z Z' f
-    simp [whiskerLeftProdMapId]
+    change prod.map (𝟙 X) f ≫ 𝟙 _ = 𝟙 _ ≫ X ◁ f
+    rw [whiskerLeftProdMapId]
+    change prod.map (𝟙 X) f ≫ 𝟙 (X ⨯ Z') = 𝟙 (X ⨯ Z) ≫ prod.map (𝟙 X) f
+    simp
 
 namespace forgetAdjStar
 
@@ -235,21 +278,28 @@ variable [HasBinaryProducts C]
 
 @[simp]
 theorem unit_app {I : C} (X : Over I): (forgetAdjStar I).unit.app X =
-    Over.homMk (prod.lift X.hom (𝟙 X.left)) := by
-  ext
-  simp [forgetAdjStar, Adjunction.comp, Equivalence.symm]
+    Over.homMk (prod.lift X.hom (𝟙 X.left)) (by
+      change prod.lift X.hom (𝟙 X.left) ≫ ((star I).obj X.left).hom = X.hom
+      rw [star_obj_hom_eq_fst]
+      exact prod.lift_fst ..) := by
+  apply Over.OverMorphism.ext
+  exact Over.forgetAdjStar_unit_app_left I X
 
 @[simp]
 theorem counit_app {I : C} (X : C) :
     ((forgetAdjStar I).counit.app X) = prod.snd := by
-  simp [Over.forgetAdjStar, Adjunction.comp, Equivalence.symm]
+  exact Over.forgetAdjStar_counit_app I X
 
 @[simp]
 theorem homEquiv_homMk_lift {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} :
     ((forgetAdjStar I).homEquiv X A) f =
-    Over.homMk (prod.lift X.hom f) := by
+    Over.homMk (prod.lift X.hom f) (by
+      rw [star_obj_hom_eq_fst]
+      exact prod.lift_fst ..) := by
   rw [Adjunction.homEquiv_unit, unit_app]
-  ext
+  apply Over.OverMorphism.ext
+  change prod.lift _ (𝟙 _) ≫ prod.map (𝟙 I) f = prod.lift _ f
+  rw [prod.lift_map]
   simp
 
 @[simp]
@@ -261,9 +311,13 @@ theorem homEquiv_left_lift {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} :
 
 theorem homEquiv_lift' {X I : C} {u : X ⟶ I} {A : C} {f : X ⟶ A} :
     ((forgetAdjStar I).homEquiv (.mk u) A) f =
-    Over.homMk (prod.lift u f) := by
+    Over.homMk (prod.lift u f) (by
+      rw [star_obj_hom_eq_fst]
+      exact prod.lift_fst ..) := by
   rw [Adjunction.homEquiv_unit, unit_app]
-  ext
+  apply Over.OverMorphism.ext
+  change prod.lift _ (𝟙 _) ≫ prod.map (𝟙 I) f = prod.lift _ f
+  rw [prod.lift_map]
   simp
 
 @[simp]
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
index 609ffd6..b9f9e37 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
@@ -106,14 +106,14 @@ def sectionsMap {X X' : Over I} (u : X ⟶ X') :
 lemma sectionsMap_id {X : Over I} : sectionsMap (𝟙 X) = 𝟙 _ := by
   apply pullback.hom_ext
   · aesop
-  · simp [sectionsMap]
+  · simp [sectionsMap, pullback.map]
 
 @[simp]
 lemma sectionsMap_comp {X X' X'' : Over I} (u : X ⟶ X') (v : X' ⟶ X'') :
     sectionsMap (u ≫ v) = sectionsMap u ≫ sectionsMap v := by
-  apply pullback.hom_ext
-  · aesop
-  · simp [sectionsMap]
+  unfold sectionsMap
+  rw [pullback.map_comp]
+  simp only [id_comp, Functor.map_comp, Over.comp_left]
 
 variable (I)
 
@@ -140,6 +140,12 @@ def sectionsCurry {X : Over I} {A : C} (u : (star I).obj A ⟶ X) :
     (MonoidalClosed.uncurry_injective _)
   rw [MonoidalClosed.uncurry_natural_left]
   simp [curryId, MonoidalClosed.uncurry_natural_right, MonoidalClosed.uncurry_curry]
+  have hu : u.left ≫ X.hom = prod.fst := (Over.w u).trans (prod.lift_fst ..)
+  calc
+    fst I A = (prodIsoTensorObj I A).inv ≫ prod.fst := prodIsoTensorObj_inv_fst.symm
+    _ = (prodIsoTensorObj I A).inv ≫ (u.left ≫ X.hom) :=
+      congrArg (fun k : I ⨯ A ⟶ I => (prodIsoTensorObj I A).inv ≫ k) hu.symm
+    _ = ((prodIsoTensorObj I A).inv ≫ u.left) ≫ X.hom := (Category.assoc _ _ _).symm
 
 /-- 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) :
@@ -147,32 +153,53 @@ def sectionsUncurry {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) :
   let v₂ : A ⟶ (I ⟹ X.left) := v ≫ pullback.snd ..
   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]
+    exact (Category.assoc _ _ _).trans
+      ((congrArg (fun k => v ≫ k)
+        (pullback.condition (f := curryId I) (g := (ihom I).map X.hom))).trans
+          (Category.assoc _ _ _).symm)
   dsimp [curryId] at w
   have w' := homEquiv_naturality_right_square (F := MonoidalCategory.tensorLeft I)
     (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]
+    change ((prodIsoTensorObj I A).hom ≫ ((ihom.adjunction I).homEquiv A X.left).symm v₂) ≫
+      X.hom = prod.lift prod.fst (𝟙 (I ⨯ A)) ≫ prod.fst
+    rw [Category.assoc, ← w', prodIsoTensorObj_hom_fst, prod.lift_fst]
+
+private theorem sectionsCurry_snd {X : Over I} {A : C} (u : (star I).obj A ⟶ X) :
+    sectionsCurry u ≫ pullback.snd (curryId I) ((ihom I).map X.hom) =
+      MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ u.left) :=
+  pullback.lift_snd ..
+
+private theorem sectionsMap_snd {X X' : Over I} (u : X ⟶ X') :
+    sectionsMap u ≫ pullback.snd (curryId I) ((ihom I).map X'.hom) =
+      pullback.snd (curryId I) ((ihom I).map X.hom) ≫ (ihom I).map u.left :=
+  pullback.lift_snd ..
 
 @[simp]
 theorem sections_curry_uncurry {X : Over I} {A : C} {v : A ⟶ (sections I).obj X} :
     sectionsCurry (sectionsUncurry v) = v := by
-  dsimp [sectionsCurry, sectionsUncurry]
-  let v₂ : A ⟶ (I ⟹ X.left) := v ≫ pullback.snd _ _
   apply pullback.hom_ext
-  · simp
-    rw [IsTerminal.hom_ext terminalIsTerminal (terminal.from A ) (v ≫ (pullback.fst ..))]
-  · simp
+  · exact terminalIsTerminal.hom_ext _ _
+  · calc
+      sectionsCurry (sectionsUncurry v) ≫ pullback.snd _ _ =
+          MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ (sectionsUncurry v).left) :=
+        sectionsCurry_snd _
+      _ = MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ (prodIsoTensorObj I A).hom ≫
+          MonoidalClosed.uncurry (v ≫ pullback.snd _ _)) := rfl
+      _ = v ≫ pullback.snd _ _ :=
+        (congrArg MonoidalClosed.curry (Iso.inv_hom_id_assoc _ _)).trans
+          (MonoidalClosed.curry_uncurry _)
 
 @[simp]
 theorem sections_uncurry_curry {X : Over I} {A : C} {u : (star I).obj A ⟶ X} :
     sectionsUncurry (sectionsCurry u) = u := by
-  dsimp [sectionsCurry, sectionsUncurry]
-  ext
-  simp
+  apply Over.OverMorphism.ext
+  exact (congrArg (fun k => (prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry k)
+    (sectionsCurry_snd u)).trans
+      ((congrArg (fun k => (prodIsoTensorObj I A).hom ≫ k)
+        (MonoidalClosed.uncurry_curry _)).trans (Iso.hom_inv_id_assoc _ _))
 
 /-- An auxiliary definition which is used to define the adjunction between the star functor
 and the sections functor. See starSectionsAdjunction`. -/
@@ -185,17 +212,31 @@ def coreHomEquiv : CoreHomEquiv (star I) (sections I) where
   }
   homEquiv_naturality_left_symm := by
     intro A' A X g v
-    dsimp [sectionsCurry, sectionsUncurry, curryId]
-    simp only [star_map]
-    rw [← Over.homMk_comp]  -- note: in a newer version of mathlib this is `Over.homMk_eta`
-    congr 1
-    simp [MonoidalClosed.uncurry_natural_left]
+    let v₂ : A ⟶ I ⟹ X.left := v ≫ pullback.snd _ _
+    have h : (prodIsoTensorObj I A').hom ≫ MonoidalClosed.uncurry (g ≫ v₂) =
+        prod.map (𝟙 I) g ≫ (prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry v₂ := by
+      rw [MonoidalClosed.uncurry_natural_left, ← Category.assoc, ← id_tensorHom,
+        ← prodMap_comp_prodIsoTensorObj_hom, Category.assoc]
+    apply Over.OverMorphism.ext
+    exact (congrArg (fun k => (prodIsoTensorObj I A').hom ≫ MonoidalClosed.uncurry k)
+      (Category.assoc g v (pullback.snd _ _))).trans h
   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 [← MonoidalClosed.curry_natural_right, Category.assoc]
+    calc
+      sectionsCurry (u ≫ g) ≫ pullback.snd _ _ =
+          MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ (u ≫ g).left) :=
+        sectionsCurry_snd _
+      _ = MonoidalClosed.curry (((prodIsoTensorObj I A).inv ≫ u.left) ≫ g.left) :=
+        congrArg MonoidalClosed.curry (Category.assoc _ _ _).symm
+      _ = MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ u.left) ≫ (ihom I).map g.left :=
+        MonoidalClosed.curry_natural_right _ _
+      _ = (sectionsCurry u ≫ pullback.snd _ _) ≫ (ihom I).map g.left :=
+        congrArg (fun k => k ≫ (ihom I).map g.left) (sectionsCurry_snd u).symm
+      _ = sectionsCurry u ≫ (pullback.snd _ _ ≫ (ihom I).map g.left) := Category.assoc _ _ _
+      _ = sectionsCurry u ≫ (sectionsMap g ≫ pullback.snd _ _) :=
+        congrArg (fun k => sectionsCurry u ≫ k) (sectionsMap_snd g).symm
+      _ = (sectionsCurry u ≫ sectionsMap g) ≫ pullback.snd _ _ := (Category.assoc _ _ _).symm
 
 variable (I)
 
diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean
index b19ae69..d8038ea 100644
--- a/Poly/ForMathlib/CategoryTheory/Elements.lean
+++ b/Poly/ForMathlib/CategoryTheory/Elements.lean
@@ -10,22 +10,22 @@ namespace CategoryTheory.CategoryOfElements
 variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟]
 variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟)
 
--- FIXME(mathlib): `NatTrans.mapElements` and `CategoryOfElements.map` are the same thing
-
 @[simp]
 theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) :
-    -- NOTE: without `α := X ⟶ X`, a bad discrimination tree key involving `⟨X, a⟩.1` is generated.
-    G.map (Subtype.mk (α := X ⟶ X) (𝟙 X) eq) = 𝟙 (G.obj ⟨X, a⟩) :=
+    G.map (X := F.elementsMk X a) (Y := F.elementsMk X a)
+      (Functor.Elements.homMk (𝟙 X) eq) = 𝟙 (G.obj (F.elementsMk X a)) :=
   show G.map (𝟙 _) = 𝟙 _ by simp
 
 @[simp]
 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 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)⟩
+    G.map (X := F.elementsMk X a) (Y := F.elementsMk Z (F.map g (F.map f a)))
+      (Functor.Elements.homMk (f ≫ g) eq) =
+    G.map (X := F.elementsMk X a) (Y := F.elementsMk Y (F.map f a))
+      (Functor.Elements.homMk f rfl) ≫
+    G.map (Functor.Elements.homMk g rfl) := by
+  set X : F.Elements := F.elementsMk X a
+  set Y : F.Elements := F.elementsMk Y (F.map f a)
+  set Z : F.Elements := F.elementsMk Z (F.map g (F.map f a))
   set f : X ⟶ Y := ⟨f, rfl⟩
   set g : Y ⟶ Z := ⟨g, rfl⟩
   show G.map (f ≫ g) = G.map f ≫ G.map g
diff --git a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
index e76ce64..1c8a96d 100644
--- a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
@@ -22,9 +22,13 @@ theorem reflect_isPullback
   let i := cospanCompIso F h i
   apply IsLimit.equivOfNatIsoOfIso i.symm pb.cone _ _ pb.isLimit
   let j :
-      ((Cones.postcompose i.symm.hom).obj pb.cone).pt ≅
+      ((Cone.postcompose i.symm.hom).obj pb.cone).pt ≅
       (F.mapCone <| PullbackCone.mk f g sq.w).pt :=
     Iso.refl _
-  apply WalkingCospan.ext j <;> simp +zetaDelta
+  apply WalkingCospan.ext j
+  · change F.map f ≫ 𝟙 _ = 𝟙 _ ≫ F.map f
+    simp
+  · change F.map g ≫ 𝟙 _ = 𝟙 _ ≫ F.map g
+    simp
 
 end CategoryTheory.Functor
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean
index c1726dd..a340cce 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean
@@ -62,8 +62,8 @@ universe v u
 
 namespace CategoryTheory
 
-open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits Functor Adjunction
-  Over
+open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits
+  CategoryTheory.Functor Adjunction Over
 
 variable {C : Type u} [Category.{v} C]
 
@@ -177,6 +177,7 @@ instance isMultiplicative : (ExponentiableMorphism (C:= C)).IsMultiplicative whe
   comp_mem f g fexp gexp := by infer_instance
 
 /-- A morphism with a pushforward is an exponentiable object in the slice category. -/
+@[instance_reducible]
 def exponentiableOverMk [HasFiniteWidePullbacks C] {X I : C} (f : X ⟶ I)
     [ExponentiableMorphism f] :
     Closed (Over.mk f) where
@@ -192,7 +193,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) [Closed X] :
+theorem 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)
@@ -282,10 +283,12 @@ 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. -/
+@[instance_reducible]
 def monoidalClosed [HasTerminal C] :
     MonoidalClosed C := cartesianClosedOfEquiv <| equivOverTerminal C
 
 /-- The slices of a locally cartesian closed category are locally cartesian closed. -/
+@[instance_reducible]
 def overLocallyCartesianClosed (I : C) : LocallyCartesianClosed (Over I) := by
   apply (config := { allowSynthFailures:= true}) mkOfCartesianClosedOver
   intro X
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean
index ff77bff..1b06775 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean
@@ -49,7 +49,7 @@ in Mathematical Structures in Computer Science, 2024][Hazratpour_Riehl_2024]
 noncomputable section
 namespace CategoryTheory
 
-open Category Functor Adjunction Limits NatTrans ExponentiableMorphism
+open Category CategoryTheory.Functor Adjunction Limits NatTrans ExponentiableMorphism
 
 universe v u
 
@@ -97,7 +97,8 @@ map k |          ↙          | map h
 -/
 --pullbackBeckChevalleySquare
 def pullbackMapTwoSquare : TwoSquare (pullback f) (map k) (map h) (pullback g) :=
-  mateEquiv (mapPullbackAdj f) (mapPullbackAdj g) (mapIsoSquare sq).hom
+  mateEquiv (mapPullbackAdj f) (mapPullbackAdj g)
+    (TwoSquare.mk _ _ _ _ (mapIsoSquare sq).hom)
 
 /--
 The natural transformation `pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C`
@@ -111,8 +112,10 @@ forget Y |          ↙          | forget X
 ```
 -/
 def pullbackForgetTwoSquare : TwoSquare (pullback f) (forget Y) (forget X) (𝟭 C) :=
-  mateEquiv (mapPullbackAdj f) Adjunction.id (mapForget f).inv
+  mateEquiv (mapPullbackAdj f) Adjunction.id
+    (TwoSquare.mk _ _ _ _ (mapForget f).inv)
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem isCartesian_pullbackForgetTwoSquare {X Y : C} (f : X ⟶ Y) :
     NatTrans.IsCartesian (pullbackForgetTwoSquare f) := by
   unfold pullbackForgetTwoSquare
@@ -282,9 +285,9 @@ theorem pullback.map_isIso_of_pullback_right_of_comm_cube {W X Y Z S T : C}
     IsIso (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ sq_bot.w pb_right.w.symm) := by
   let m := pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ sq_bot.w pb_right.w.symm
   have sq_top : CommSq (pullback.snd f₁ f₂) m i₂ (pullback.snd g₁ g₂) := by
-    aesop
+    exact ⟨by simp [m, pullback.map, pullback.lift_snd]⟩
   have sq_left : CommSq m (pullback.fst f₁ f₂) (pullback.fst g₁ g₂) i₁ := by
-    aesop
+    exact ⟨by simp [m, pullback.map, pullback.lift_fst]⟩
   let pb' : IsPullback m (pullback.fst f₁ f₂)  (pullback.fst g₁ g₂) i₁ := by
     apply IsPullback.left_face_of_comm_cube (sq_top := sq_top) (sq_bot := sq_bot)
       (sq_left := sq_left) (pb_back := (IsPullback.of_hasPullback f₁ f₂).flip)
@@ -298,7 +301,7 @@ end IsPullback
 variable [HasPullbacks C]
 
 variable {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y}  {g : Z ⟶ W} {k : Y ⟶ W}
-(sq : CommSq h f g k) (A : Over Y)
+  (sq : CommSq h f g k) (A : Over Y)
 
 open IsPullback Over
 
@@ -309,10 +312,11 @@ theorem mapPullbackAdj.counit_app_left  :
 @[simp]
 theorem pullbackMapTwoSquare_app :
     (pullbackMapTwoSquare h f g k sq).app A =
-    Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by aesop) := by
+    Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by simp [pullback.map, pullback.lift_snd]) := by
   ext
-  simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare]
-  aesop
+  simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare, mateEquiv_apply]
+  apply pullback.hom_ext <;>
+    simp [pullback.map, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc, Category.assoc]
 
 theorem forget_map_pullbackMapTwoSquare :
     (Over.forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) =
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
index ac406aa..8b7ebcb 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
@@ -29,7 +29,7 @@ We construct a natural isomorphism
 noncomputable section
 namespace CategoryTheory
 
-open Category Functor Adjunction Limits NatTrans Over ExponentiableMorphism Reindex
+open Category CategoryTheory.Functor Adjunction Limits NatTrans Over ExponentiableMorphism Reindex
   LocallyCartesianClosed
 
 universe v u
@@ -50,7 +50,7 @@ exponentiable morphisms, we'll usually prove all morphims are exponential unifor
 from LocallyCartesianClosed structure.
 The instance is inferred from the LocallyCartesianClosed structure, but
 we should prove this more generally without assuming the LCCC structure. -/
-def exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance
+theorem exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance
 
 namespace ExponentiableMorphism
 
@@ -61,10 +61,14 @@ def mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F :
   have := congr($((whiskerLeft_comp_whiskerRight η η)).app X)
   refine ⟨_, _, _, this, Fork.IsLimit.mk' _ fun s => ?_⟩
   have hi := (Fork.ι s).w; simp at hi
-  have w := congr($(Fork.condition s).left ≫ pullback.fst .. ≫ pullback.snd ..); simp [η] at w
+  have w := congr($(Fork.condition s).left ≫ pullback.fst .. ≫ pullback.snd ..)
+  simp [η, pullback.lift_snd, pullback.lift_fst_assoc] at w
   refine ⟨homMk (s.ι.left ≫ pullback.fst ..) (by simp [w, hi]), ?_, ?_⟩
-  · ext; simp; ext <;> simp [η]; rw [w]
-  · intro m H; ext; simpa [η] using congr(($H).left ≫ pullback.fst ..)
+  · ext; simp; ext <;> simp [η, pullback.lift_fst, pullback.lift_snd]; rw [w]
+  · intro m H
+    ext
+    simpa [η, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc] using
+      congr(($H).left ≫ pullback.fst ..)
 
 /-- The pullback of exponentiable morphisms is exponentiable. -/
 theorem of_isPullback {C' : Type u} [Category.{v} C'] [HasPullbacks C'] [HasTerminal C']
@@ -99,7 +103,7 @@ We show that the pasting of the 2-cells in below is an isomorphism.
   so the 2-cell is an iso.
 -/
 
-def cellLeftTriangle : e f u ≫ u = w f u := by
+theorem cellLeftTriangle : e f u ≫ u = w f u := by
   unfold e w v
   have := ((ev f).app (Over.mk u)).w
   aesop_cat
@@ -116,7 +120,7 @@ lemma isCartesian_cellLeft : IsCartesian (cellLeft f u) := by
   simp only [id_obj, mk_left] at α u
   sorry
 
-def cellRightCommSq : CommSq (g f u) (w f u) (v f u) f :=
+theorem cellRightCommSq : CommSq (g f u) (w f u) (v f u) f :=
   IsPullback.toCommSq (IsPullback.of_hasPullback _ _)
 
 def cellRight' : pushforward (g f u) ⋙ map (v f u)
@@ -137,7 +141,7 @@ def pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f
 
 def pasteCell := pasteCell1 f u ≫ pasteCell2 f u
 
-def paste : IsCartesian (pasteCell f u) := by
+theorem paste : IsCartesian (pasteCell f u) := by
   apply IsCartesian.comp
   · unfold pasteCell1
     apply (isCartesian_cellRight' f u).whiskerLeft
diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean
index fea7cc5..151e0ac 100644
--- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean
+++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean
@@ -19,7 +19,7 @@ variable {K : Type*} [Category K] {D : Type*} [Category D]
 
 namespace NatTrans
 
-open Functor
+open CategoryTheory.Functor
 
 /-- A natural transformation is *cartesian*
 if all its naturality squares are pullbacks. -/
diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
index e33d783..7a2a2ac 100644
--- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
+++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
@@ -21,7 +21,7 @@ noncomputable section
 
 namespace CategoryTheory
 
-open CategoryTheory Category Limits Functor Over
+open CategoryTheory Category Limits CategoryTheory.Functor Over
 
 
 variable {C : Type*} [Category C] [HasPullbacks C]
@@ -66,7 +66,11 @@ def Fan.overPullbackToStar [HasBinaryProducts C] (c : Fan s X)  :
 @[reassoc (attr := simp)]
 theorem Fan.overPullbackToStar_snd {c : Fan s X} [HasBinaryProducts C] :
     (Fan.overPullbackToStar c).left ≫ prod.snd = c.snd := by
-  simp [Fan.overPullbackToStar, Adjunction.homEquiv, forgetAdjStar.unit_app]
+  change ((forgetAdjStar E).homEquiv ((Over.pullback s).obj c.over) X c.snd).left ≫
+    prod.snd = c.snd
+  exact (congrArg (fun k => k ≫ prod.snd)
+    (forgetAdjStar.homEquiv_left_lift (I := E) (X := (Over.pullback s).obj c.over)
+      (f := c.snd))).trans (prod.lift_snd _ _)
 
 -- note: the reason we use `(Over.pullback s).map` instead of `pullback.map` is that
 -- we want to readily use lemmas about the adjunction `pullback s ⊣ pushforward s` in `UvPoly`.
@@ -110,7 +114,8 @@ instance : Category (Fan s X) where
     rw [← f.w_right, ← g.w_right]
     simp_rw [← Category.assoc]
     congr 1
-    ext <;> simp [pullbackMap]
+    ext <;> simp [pullbackMap, pullback.lift_fst, pullback.lift_snd,
+      pullback.lift_fst_assoc, Category.assoc]
   ⟩
   id_comp f := by dsimp; ext; simp
   comp_id f := by dsimp; ext; simp
@@ -165,9 +170,7 @@ def overPullbackToStar [HasBinaryProducts C] {W} (f : W ⟶ B) (g : pullback f s
 theorem overPullbackToStar_prod_snd [HasBinaryProducts C]
     {W} {f : W ⟶ B} {g : pullback f s ⟶ X} :
     (overPullbackToStar f g).left ≫ prod.snd = g := by
-  simp only [overPullbackToStar, Fan.overPullbackToStar, Fan.over]
-  simp only [forgetAdjStar.homEquiv_left_lift]
-  aesop
+  exact Fan.overPullbackToStar_snd (c := Fan.mk f g)
 
 abbrev partialProd (c : LimitFan s X) : C := c.cone.pt
 
@@ -197,7 +200,8 @@ theorem partialProd.lift_snd {W} (c : LimitFan s X) (f : W ⟶ B) (g : pullback
   conv_rhs => arg 2; exact ((isLimit c).fac_right (Fan.mk f g)).symm
   rw [← pullbackMap_comparison]
   rw [← Category.assoc]; congr 1
-  ext <;> simp [pullbackMap]
+  ext <;> simp [pullbackMap, pullback.lift_fst, pullback.lift_snd,
+    pullback.lift_fst_assoc, pullback.map, Category.assoc]
 
 -- theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.pt) :
 --     m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b } } :=
@@ -211,5 +215,6 @@ theorem partialProd.hom_ext {W : C} (c : LimitFan s X) {f g : W ⟶ partialProd
   cases c.isLimit.uniq f' g (by simp [h₁, f']) <| by
     refine .trans ?_ h₂.symm
     rw [← Category.assoc]; congr 1
-    ext <;> simp [pullbackMap, comparison, f']
+    ext <;> simp [pullbackMap, comparison, f', pullback.lift_fst, pullback.lift_snd,
+      pullback.lift_fst_assoc, pullback.map, Category.assoc]
   exact c.isLimit.uniq f' f rfl rfl
diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean
index 3eb6659..6043294 100644
--- a/Poly/ForMathlib/CategoryTheory/Types.lean
+++ b/Poly/ForMathlib/CategoryTheory/Types.lean
@@ -21,18 +21,18 @@ variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] (F G : 𝒞 ⥤ 
 
 theorem naturality₂_left (σ : F ⟶ G) (f : C₁ ⟶ C₂) (x : (F.obj C₁).obj D₁) :
     (σ.app C₂).app D₁ ((F.map f).app D₁ x) = (G.map f).app D₁ ((σ.app C₁).app D₁ x) :=
-  congr_fun (congr_fun (congr_arg NatTrans.app (σ.naturality f)) D₁) x
+  types_congr_hom (congrArg (fun η => η.app D₁) (σ.naturality f)) x
 
 theorem naturality₂_right (σ : F ⟶ G) (f : D₁ ⟶ D₂) (x : (F.obj C₁).obj D₁) :
     (σ.app C₁).app D₂ ((F.obj C₁).map f x) = (G.obj C₁).map f ((σ.app C₁).app D₁ x) :=
-  naturality ..
+  ConcreteCategory.congr_hom ((σ.app C₁).naturality f) x
 
 @[simp]
 theorem hom_inv_id_app_app_apply (α : F ≅ G) (C D) (x) :
     (α.inv.app C).app D ((α.hom.app C).app D x) = x :=
-  congr_fun (α.hom_inv_id_app_app C D) x
+  ConcreteCategory.congr_hom (α.hom_inv_id_app_app C D) x
 
 @[simp]
 theorem inv_hom_id_app_app_apply (α : F ≅ G) (C D) (x) :
     (α.hom.app C).app D ((α.inv.app C).app D x) = x :=
-  congr_fun (α.inv_hom_id_app_app C D) x
+  ConcreteCategory.congr_hom (α.inv_hom_id_app_app C D) x
diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean
index 3edc114..6d17554 100644
--- a/Poly/MvPoly/Basic.lean
+++ b/Poly/MvPoly/Basic.lean
@@ -26,7 +26,7 @@ noncomputable section
 
 namespace CategoryTheory
 
-open CategoryTheory Category Limits Functor Adjunction ExponentiableMorphism
+open CategoryTheory Category Limits CategoryTheory.Functor Adjunction ExponentiableMorphism
 
 variable {C : Type*} [Category C] [HasPullbacks C] [HasTerminal C] [HasFiniteWidePullbacks C]
 
diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean
index 0bb4cbe..89fa2aa 100644
--- a/Poly/Type/Univariate.lean
+++ b/Poly/Type/Univariate.lean
@@ -98,8 +98,8 @@ def sumTotalEquiv (P Q : Poly) : Total (sum P Q) ≃ Total P ⊕ Total Q where
     | Sum.inl ⟨b, e⟩ => ⟨Sum.inl b, e⟩
     | Sum.inr ⟨c, f⟩ => ⟨Sum.inr c, f⟩
   left_inv := by
-    simp
-    aesop_cat
+    rintro ⟨b, e⟩
+    cases b <;> rfl
   right_inv := by aesop_cat
 
 /-- The bundle associated to a polynomial `P`. -/
@@ -177,7 +177,7 @@ theorem map_map (f : X → Y) (g : Y → Z) :
 /-- The associated functor of `P : Poly`. -/
 def functor : Type u ⥤ Type u where
   obj X := P X
-  map {X Y} f := P.map f
+  map {X Y} f := TypeCat.ofHom (P.map f)
 
 variable {P}
 
@@ -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]
+  simp only [Obj.iget, fst_map, *, dite_eq_left]
   cases x
   rfl
 
@@ -224,12 +224,12 @@ def comp.mk {X : Type u} (x : P (Q X)) : Q.comp P X :=
 /-- Functor composition for polynomial functors in the diagrammatic order. -/
 def comp.functor : Poly.functor (Q.comp P) ≅ Poly.functor Q ⋙ Poly.functor P where
   hom := {
-    app := fun X => fun ⟨b,e⟩ =>
+    app := fun X => TypeCat.ofHom fun ⟨b,e⟩ =>
     ⟨ b.1, fun x' => ⟨ b.2 x', fun b' => e ⟨x',b'⟩ ⟩⟩
     naturality := by aesop_cat
   }
   inv := {
-    app X := comp.mk P Q
+    app X := TypeCat.ofHom (comp.mk P Q)
     naturality := by aesop_cat
   }
 
diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean
index 74e0d4f..df28252 100644
--- a/Poly/UvPoly/Basic.lean
+++ b/Poly/UvPoly/Basic.lean
@@ -37,7 +37,7 @@ noncomputable section
 
 namespace CategoryTheory
 
-open Category Limits Functor Adjunction Over ExponentiableMorphism
+open Category Limits CategoryTheory.Functor Adjunction Over ExponentiableMorphism
   LocallyCartesianClosed
 
 variable {C : Type*} [Category C] [HasPullbacks C]
@@ -134,10 +134,11 @@ C --- >  C/E ---->  C/B ----> C
 def verticalNatTrans {F : C} (P : UvPoly E B) (Q : UvPoly F B) (ρ : E ⟶ F) (h : P.p = ρ ≫ Q.p) :
     Q.functor ⟶ P.functor := by
   have sq : CommSq ρ P.p Q.p (𝟙 _) := by simp [h]
-  let cellLeft := (Over.starPullbackIsoStar ρ).hom
+  let cellLeft : TwoSquare (star F) (𝟭 C) (Over.pullback ρ) (star E) :=
+    (Over.starPullbackIsoStar ρ).hom
   let cellMid := (pushforwardPullbackTwoSquare ρ P.p Q.p (𝟙 _) sq)
   let cellLeftMidPasted := TwoSquare.whiskerRight (cellLeft ≫ₕ cellMid) (Over.pullbackId).inv
-  simpa using (cellLeftMidPasted ≫ₕ (vId (Over.forget B)))
+  exact (cellLeftMidPasted ≫ₕ (vId (Over.forget B))).natTrans
 
 /-- A cartesian map of polynomials
 ```
@@ -269,7 +270,7 @@ variable {E B : C}
 
 namespace PartialProduct
 
-open PartialProduct
+open CategoryTheory.PartialProduct
 
 /-- The counit of the adjunction `pullback P.p ⊣ pushforward P.p` evaluated `(star E).obj X`. -/
 def ε (P : UvPoly E B) (X : C) : pullback (P.fstProj X) P.p ⟶ E ⨯ X :=
@@ -284,13 +285,16 @@ def fan (P : UvPoly E B) (X : C) : PartialProduct.Fan P.p X where
 
 attribute [simp] fan_pt fan_fst
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 `P.PartialProduct.fan` is in fact a limit fan; this provides the univeral mapping property of the
 polynomial functor.
 -/
 def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct.fan P X) where
   lift c := (pushforwardCurry <| overPullbackToStar c.fst c.snd).left
-  fac_left := by aesop_cat (add norm fstProj)
+  fac_left := by
+    intro c
+    exact Over.w (pushforwardCurry (overPullbackToStar c.fst c.snd))
   fac_right := by
     intro c
     simp only [fan_snd, PartialProduct.pullbackMap, ε, ev, ← assoc, ← comp_left]
@@ -307,13 +311,13 @@ def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct
     simp [overPullbackToStar, PartialProduct.Fan.overPullbackToStar, PartialProduct.Fan.over]
     apply (Adjunction.homEquiv_apply_eq _ _ _).mpr
     rw [← h_right]
-    simp [forgetAdjStar, comp_homEquiv, Comonad.adj]
-    simp [Equivalence.toAdjunction, homEquiv]
-    simp [coalgebraEquivOver, Equivalence.symm]; rfl
+    rw [Adjunction.homEquiv_counit (forgetAdjStar E)]
+    simp [homEquiv_counit, PartialProduct.pullbackMap, fan_snd, ε, ev, Category.assoc]
+    rfl
 
 end PartialProduct
 
-open PartialProduct
+open CategoryTheory.UvPoly.PartialProduct
 
 /-- Morphisms `b : Γ ⟶ B` and `e : pullback b P.p ⟶ X` induce a morphism `Γ ⟶ P @ X` which is the
 lift of the partial product fan. -/
@@ -353,28 +357,31 @@ theorem proj_fst {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} :
 @[simp]
 theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} :
     (proj P f).snd = pullback.map _ _ _ _ f (𝟙 E) (𝟙 B) (by simp) (by simp) ≫ (fan P X).snd := by
-  simp [proj]
+  rfl
 
 /-- The domain of the composition of two polynomials. See `UvPoly.comp`. -/
 def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) :=
   Limits.pullback Q.p (fan P A).snd
 
 @[simps!]
-def comp [HasPullbacks C] [HasTerminal C]
+def comp
     {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) where
   p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p
-  exp :=
-    haveI := ExponentiableMorphism.of_isPullback (.flip <| .of_hasPullback Q.p (fan P A).snd)
-    haveI := ExponentiableMorphism.of_isPullback (.of_hasPullback (fan P A).fst P.p)
-    inferInstance
+  exp := by
+    have : ExponentiableMorphism (pullback.snd Q.p (fan P A).snd) :=
+      ExponentiableMorphism.of_isPullback (.flip <| .of_hasPullback Q.p (fan P A).snd)
+    have : ExponentiableMorphism (pullback.fst (fan P A).fst P.p) :=
+      ExponentiableMorphism.of_isPullback (.of_hasPullback (fan P A).fst P.p)
+    exact ExponentiableMorphism.comp
+      (pullback.snd Q.p (fan P A).snd) (pullback.fst (fan P A).fst P.p)
 
 /-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/
-def compFunctorIso [HasPullbacks C] [HasTerminal C]
+def compFunctorIso
     {E B D C : C} (P : UvPoly E B) (Q : UvPoly D C) :
     P.functor ⋙ Q.functor ≅ (comp P Q).functor := by
   sorry
 
-instance monoidal [HasPullbacks C] [HasTerminal C] : MonoidalCategory (UvPoly.Total C) where
+instance monoidal : MonoidalCategory (UvPoly.Total C) where
   tensorObj X Y := ⟨comp X.poly Y.poly⟩
   whiskerLeft X Y₁ Y₂ := sorry
   whiskerRight := sorry
diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean
index 4ccc736..cf9c656 100644
--- a/Poly/UvPoly/UPFan.lean
+++ b/Poly/UvPoly/UPFan.lean
@@ -8,7 +8,7 @@ import Poly.UvPoly.Basic
 noncomputable section
 
 namespace CategoryTheory.UvPoly
-open Limits PartialProduct
+open Limits CategoryTheory.UvPoly.PartialProduct
 
 universe v u
 variable {C : Type u} [Category.{v} C] [HasPullbacks C] [HasTerminal C] {E B : C}
diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean
index 4843fd9..6a7c940 100644
--- a/Poly/UvPoly/UPIso.lean
+++ b/Poly/UvPoly/UPIso.lean
@@ -9,7 +9,7 @@ import Poly.Bifunctor.Sigma
 noncomputable section
 
 namespace CategoryTheory.UvPoly
-open Limits Over ExponentiableMorphism Functor
+open Limits Over ExponentiableMorphism CategoryTheory.Functor
 
 universe v u
 variable {C : Type u} [Category.{v} C] [HasPullbacks C] {E B : C} (P : UvPoly E B)
@@ -25,13 +25,17 @@ def partProdsOver : Cᵒᵖ ⥤ C ⥤ Type v :=
 @[simp]
 theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.partProdsOver.obj Γ).obj X) :
     (P.partProdsOver.obj Γ).map f x = ⟨x.1, x.2 ≫ f⟩ := by
-  dsimp [partProdsOver]
+  dsimp +instances [partProdsOver, Functor.Sigma]
   have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp
   ext : 1
   . simp
   . dsimp
     rw! (castMode := .all) [this]
     simp
+    change pullback.lift (f := x.1) (g := P.p) (pullback.fst x.1 P.p ≫ 𝟙 _) (pullback.snd x.1 P.p) _ ≫
+      x.2 ≫ f = x.2 ≫ f
+    simp
+    rfl
 
 variable [HasTerminal C]
 
@@ -73,7 +77,7 @@ def equiv (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback
 
 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]
+  rfl
 
 lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) :
     P.equiv Δ X (σ ≫ be) =
@@ -82,6 +86,7 @@ lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.
         (Category.assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by
   conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_left, ← equiv_app]
   simp
+  rfl
 
 -- 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) :
@@ -89,6 +94,6 @@ lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X 
       let p := equiv P Γ X be
       ⟨p.1, p.2 ≫ f⟩ := by
   conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_right, ← equiv_app]
-  simp
+  exact P.partProdsOver_obj_map (.op Γ) f (P.equiv Γ X be)
 
 end CategoryTheory.UvPoly
diff --git a/Poly/Widget/CommDiag.lean b/Poly/Widget/CommDiag.lean
index cbb13bf..aca4512 100644
--- a/Poly/Widget/CommDiag.lean
+++ b/Poly/Widget/CommDiag.lean
@@ -3,9 +3,10 @@ Copyright (c) 2024 Wojciech Nawrocki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
-import ProofWidgets.Component.GraphDisplay
+import ProofWidgets.Component.ForceGraphDisplay
 import ProofWidgets.Component.Panel.SelectionPanel
 import ProofWidgets.Component.Panel.GoalTypePanel
+import ProofWidgets.Presentation.Expr
 import Mathlib.CategoryTheory.Category.Basic
 
 /-! ## Definitions copied from Mathlib.Tactic.Widget.CommDiag
@@ -70,9 +71,9 @@ where go (f : Expr) : MetaM (List (Expr × Expr)) := do
 
 structure DiagState where
   /-- vertex id ↦ object -/
-  vertices: Std.HashMap Nat Expr := .empty
+  vertices: Std.HashMap Nat Expr := {}
   /-- morphism `f` ↦ (src, tgt) for every occurrence of `f` -/
-  edges: Std.HashMap Expr (List (Nat × Nat)) := .empty
+  edges: Std.HashMap Expr (List (Nat × Nat)) := {}
   freshVertId : Nat := 0
 
 variable {m : Type → Type} [Monad m] [MonadStateOf DiagState m]
@@ -144,7 +145,7 @@ def addEq [MonadLift MetaM m] (eq : Expr) : m Unit := do
 
 open Jsx in
 def mkLabel (e : Expr) : MetaM (Nat × Nat × Html) := do
-  let fmt ← withOptions (·.setNat `pp.deepTerms.threshold 1)
+  let fmt ← withOptions (·.set `pp.deepTerms.threshold (1 : Nat))
     (toString <$> ppExpr e)
   let w := min (15 + fmt.length * 6) 100
   let h := max 20 (20 * (1 + fmt.length / 15))
@@ -194,7 +195,7 @@ def toHtml [MonadLift MetaM m] : m Html := do
             <br/>
           </span>
       }
-  return <GraphDisplay
+  return <ForceGraphDisplay
     vertices={vertices}
     edges={edges}
     forces={#[
diff --git a/README.md b/README.md
index cdf751b..c95ea3a 100644
--- a/README.md
+++ b/README.md
@@ -1,10 +1,10 @@
 [![License: Apache 2.0](https://img.shields.io/badge/License-Apache_2.0-lightblue.svg)](https://opensource.org/licenses/Apache-2.0)
-[![Documentation](https://img.shields.io/badge/Documentation-Passing-green)](https://sinhp.github.io/groupoid_model_in_lean4/docs/Poly/UvPoly.html)
-[![Paper](https://img.shields.io/badge/Paper-WIP-blue)](https://sinhp.github.io/groupoid_model_in_lean4/blueprint/sect0005.html)
+[![Documentation](https://img.shields.io/badge/Documentation-blue)](https://sinhp.github.io/Poly/docs/)
+[![Blueprint](https://img.shields.io/badge/Blueprint-WIP-blue)](https://sinhp.github.io/Poly/blueprint/)
 
-[Proofs Verified with Lean4 (leanprover/lean4:v4.18.0-rc1)](https://github.com/sinhp/LeanHomotopyFrobenius/blob/master/lean-toolchain)
+[Built with Lean 4.34.1](lean-toolchain)
 
-# Lean4 Formalization Of Polynomial Functors
+# Lean 4 Formalization of Polynomial Functors
 
 This repository is a [Lean 4](https://github.com/leanprover/lean4) formalization of the theory of Polynomial Functors. Polynomial Functors categorify polynomial functions.
 
@@ -12,6 +12,8 @@ We use this repository as a dependency in the [HoTTLean](https://github.com/sinh
 
 ## Content (under development)
 
+Some constructions still contain unfinished proofs.
+
 As part of this formalization, we also formalize locally cartesian closed categories in Lean4.
 
 - [x] Locally cartesian closed categories
@@ -45,7 +47,7 @@ As part of this formalization, we also formalize locally cartesian closed catego
   - [ ] The double category of polynomial functors
   - [ ] Differentiation
 
-- [ ] Induction, Well-foundedtrees, Transfinite Induction
+- [ ] Induction, Well-founded trees, Transfinite Induction
 
 - [ ] Polynomial functors and the semantics of linear logic
   - [ ] A relational presentation of polynomial functors
diff --git a/lake-manifest.json b/lake-manifest.json
index f32e2f9..10a4c1b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,31 +1,28 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/PatrickMassot/checkdecls.git",
-   "type": "git",
-   "subDir": null,
+ [{"type": "path",
    "scope": "",
-   "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
    "inherited": false,
+   "dir": "vendor/checkdecls",
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b8dad038b1b3a05b77d6884b15b8db03ec01dca1",
+   "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.34.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
+   "rev": "e928b72544873815af278d38681b31c0293588e3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +52,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.86",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
+   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "100083c18750b6a9b7553c65f6b052c0a2f6bcb4",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,11 +92,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.34.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.lean b/lakefile.lean
index ae32354..ab6445a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -9,14 +9,14 @@ package Poly where
   -- add any additional package configuration options here
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.34.1"
 
 @[default_target]
 lean_lib Poly where
   -- add any library configuration options here
 
-require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
+require checkdecls from "vendor/checkdecls"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.27.0-rc1"
+  "https://github.com/leanprover/doc-gen4" @ "v4.34.1"
diff --git a/lean-toolchain b/lean-toolchain
index 3e9b4e1..ba8ebf2 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.28.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.34.1
diff --git a/vendor/checkdecls/.gitignore b/vendor/checkdecls/.gitignore
new file mode 100644
index 0000000..3d1e18d
--- /dev/null
+++ b/vendor/checkdecls/.gitignore
@@ -0,0 +1,4 @@
+/build
+/lakefile.olean
+/lake-packages/*
+.lake
diff --git a/vendor/checkdecls/LICENSE b/vendor/checkdecls/LICENSE
new file mode 100644
index 0000000..8dada3e
--- /dev/null
+++ b/vendor/checkdecls/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "{}"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright {yyyy} {name of copyright owner}
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/vendor/checkdecls/Main.lean b/vendor/checkdecls/Main.lean
new file mode 100644
index 0000000..ceab749
--- /dev/null
+++ b/vendor/checkdecls/Main.lean
@@ -0,0 +1,26 @@
+import Lake.CLI.Main
+open Lake Lean
+
+unsafe def main (args : List String) : IO UInt32 := do
+  unless args.length == 1 do
+    println! "This command takes exactly one argument: the path to a file containing a list of declarations to check."
+    return 1
+  let filename : System.FilePath := args[0]!
+  unless ← filename.pathExists do
+    println! "Could not find declaration list {filename}."
+    return 1
+  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
+  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+  let (ws?, log) ← (loadWorkspace config).run?
+  log.replay (logger := .stderr)
+  let some ws := ws? | return 1
+  let imports := ws.root.leanLibs.flatMap (·.config.roots.map fun module => { module })
+  -- see comments in https://github.com/leanprover/lean4/pull/6325
+  enableInitializersExecution
+  let env ← Lean.importModules imports {}
+  let mut ok := true
+  for line in ← IO.FS.lines filename do
+    unless env.contains line.toName do
+      println! "{line} is missing."
+      ok := false
+  return if ok then 0 else 1
diff --git a/vendor/checkdecls/UPSTREAM.md b/vendor/checkdecls/UPSTREAM.md
new file mode 100644
index 0000000..252a285
--- /dev/null
+++ b/vendor/checkdecls/UPSTREAM.md
@@ -0,0 +1,25 @@
+# checkdecls provenance and Lean migration
+
+Vendored from https://github.com/PatrickMassot/checkdecls at commit
+`3d425859e73fcfbef85b9638c2a91708ef4a22d4` (tag `lean4.18.0`, upstream
+`master` as observed on 2026-10-10). Upstream had no Lean v4.34.1 release or
+branch. The original Apache-2.0 license is retained in `LICENSE`.
+
+Changes made for Poly's Lean v4.34.1 migration:
+
+- Updated `lean-toolchain` from `leanprover/lean4:v4.18.0` to
+  `leanprover/lean4:v4.34.1`.
+- Ran `lake update`; Lake rewrote the empty manifest to schema 1.2.0 and
+  added `fixedToolchain: false`. This package has no dependency repositories.
+- No edits to `Main.lean` or `lakefile.lean` were required.
+
+Verification on 2026-10-10 with Lean v4.34.1 on Linux:
+
+- Standalone `lake update`: exit 0.
+- Standalone `lake build`: exit 0, 4 jobs, no warnings.
+- Executable smoke test in a separate tiny Lean package: an imported, existing
+  declaration returned 0; an absent declaration returned 1 with its name;
+  a nonexistent declaration-list file returned 1; no arguments returned 1.
+
+The dependency is stored as ordinary source files, rather than an embedded Git
+repository, so Poly's relative `vendor/checkdecls` path dependency is portable.
diff --git a/vendor/checkdecls/lake-manifest.json b/vendor/checkdecls/lake-manifest.json
new file mode 100644
index 0000000..2f2af5a
--- /dev/null
+++ b/vendor/checkdecls/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "checkdecls",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/vendor/checkdecls/lakefile.lean b/vendor/checkdecls/lakefile.lean
new file mode 100644
index 0000000..e28ea0a
--- /dev/null
+++ b/vendor/checkdecls/lakefile.lean
@@ -0,0 +1,13 @@
+import Lake
+open Lake DSL
+
+package «checkdecls» {
+  -- add package configuration options here
+}
+
+@[default_target]
+lean_exe «checkdecls» {
+  root := `Main
+  supportInterpreter := true
+  weakLinkArgs := #["-lLake"]
+}
diff --git a/vendor/checkdecls/lean-toolchain b/vendor/checkdecls/lean-toolchain
new file mode 100644
index 0000000..ba8ebf2
--- /dev/null
+++ b/vendor/checkdecls/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1