diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean
index 17503a9..e72b2a5 100644
--- a/Poly/Bifunctor/Basic.lean
+++ b/Poly/Bifunctor/Basic.lean
@@ -16,7 +16,7 @@ variable {𝒞 𝒟' 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟'] [Categor
 
 /-- Precompose a bifunctor in the second argument.
 Note that `G ⋙₂ F ⋙ P = F ⋙ G ⋙₂ P` definitionally. -/
-@[simps]
+@[implicit_reducible, simps]
 def comp₂ (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where
   obj Γ := F ⋙ P.obj Γ
   map f := whiskerLeft F (P.map f)
@@ -69,13 +69,13 @@ namespace coyoneda
 theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
     (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]
+    (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) :=
+  FunctorToTypes.naturality₂_left ..
 
 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]
+    (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) :=
+  FunctorToTypes.naturality₂_right ..
 
 end coyoneda
 
@@ -87,8 +87,8 @@ 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 _ _ => by ext x; simp [A.homEquiv_naturality_left])
+    (fun _ _ => by ext x; simp [A.homEquiv_naturality_right])
 
 end Adjunction
 end CategoryTheory
diff --git a/Poly/Bifunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean
index d453d2d..3460514 100644
--- a/Poly/Bifunctor/Sigma.lean
+++ b/Poly/Bifunctor/Sigma.lean
@@ -13,6 +13,10 @@ import Poly.Bifunctor.Basic
 
 /-! ## Dependent sums of functors -/
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching, which stops them
+-- reducing through `Functor.Elements` (a `def` over `Sigma`) and the `TypeCat.Hom` wrapper.
+set_option backward.isDefEq.respectTransparency false
+
 namespace CategoryTheory.Functor
 
 universe w v u t s r
@@ -46,18 +50,24 @@ a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward.
 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)⟩
+    map := fun (f, g) => ↾(fun ⟨a, b⟩ =>
+      ⟨F.map f a, (G.map ⟨f, rfl⟩).app _ ((G.obj ⟨_, a⟩).map g b)⟩)
     map_id := ?_
     map_comp := ?_
-  } <;> {
-    intros
-    ext ⟨a, b⟩ : 1
+  }
+  -- The objects must be destructured before the `match` on morphisms of `𝒞 × 𝒟` reduces.
+  · rintro ⟨X₁, X₂⟩
+    ext ⟨a, b⟩ : 3
+    dsimp
+    congr! 1 with h
+    . simp
+    . rw! [h]; simp [FunctorToTypes.naturality]
+  · rintro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ ⟨Z₁, Z₂⟩ ⟨f₁, f₂⟩ ⟨g₁, g₂⟩
+    ext ⟨a, b⟩ : 3
     dsimp
     congr! 1 with h
     . simp
     . rw! [h]; simp [FunctorToTypes.naturality]
-  }
 
 def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
     /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements`
@@ -70,17 +80,15 @@ def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
     (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
+      left_inv := by rintro ⟨_, _⟩; refine Sigma.ext ?_ ?_ <;> simp
+      right_inv := by rintro ⟨_, _⟩; refine Sigma.ext ?_ ?_ <;> simp
     }) ?_ ?_ <;> {
       intros
-      ext : 1
-      dsimp
-      apply have h := ?_; Sigma.ext h ?_
-      . simp [FunctorToTypes.naturality]
-      . dsimp [Sigma] at h ⊢
-        rw! [← h]
-        simp [NatTrans.mapElements]
+      ext ⟨a, b⟩ : 3
+      dsimp [Sigma, Equiv.toIso, NatTrans.mapElements]
+      congr! 1 with h
+      . simp
+      . rw! [← h]; simp
     }
 
 def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type v} (i : G₁ ≅ G₂) :
@@ -93,12 +101,9 @@ def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 
       right_inv := fun ⟨_, _⟩ => by simp
     }) ?_ ?_ <;> {
       intros
-      ext : 1
-      dsimp
-      apply have h := ?_; Sigma.ext h ?_
-      . simp
-      . dsimp [Sigma] at h ⊢
-        simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right]
+      ext ⟨a, b⟩ : 3
+      dsimp [Sigma, Equiv.toIso]
+      simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right]
     }
 
 theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
@@ -110,13 +115,11 @@ theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
     . intro; simp
     . intros
       apply heq_of_eq
-      ext : 1
-      apply Sigma.ext <;> simp
-  . intros
-    apply heq_of_eq
-    ext : 3
-    apply Sigma.ext <;> simp
-
+      ext ⟨a, b⟩ : 3 <;> dsimp [Sigma]
+  . intro X Y f
+    have h : (G ⋙₂ Sigma P).map f = (Sigma (G ⋙₂ P)).map f := by
+      ext D ⟨a, b⟩ : 5 <;> simp [Sigma]
+    exact heq_of_eq h
 end CategoryTheory.Functor
 
 /-! ## Over categories -/
@@ -137,6 +140,12 @@ def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X 
     . simp
     . rw! [h]; simp
 
+/-- Bridge between the `Equiv` and the `Type`-category morphism it induces, so that the
+`@[simps]` lemmas for `equiv_Sigma` fire under `Equiv.toIso`. -/
+@[simp]
+lemma equiv_Sigma_toIso_hom_apply {A : 𝒞} (X : 𝒞) (U : Over A) (g : X ⟶ U.left) :
+    (ConcreteCategory.hom (equiv_Sigma X U).toIso.hom) g = equiv_Sigma X U g := rfl
+
 @[simps]
 def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ where
   functor := {
@@ -158,20 +167,20 @@ def forget_iso_Sigma (A : 𝒞) :
     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 have h := ?_; Sigma.ext h ?_
+    ext x : 3
+    dsimp [Functor.Sigma, equivalence_Elements, coyoneda]
+    congr! 1 with h
     . simp
-    . dsimp at h ⊢
-      rw! [h]
+    . rw! [← h]
+      apply heq_of_eq
+      ext : 1
       simp
   . intros X Y U f
-    ext : 1
-    dsimp
-    apply have h := ?_; Sigma.ext h ?_
+    ext x : 3
+    dsimp [Functor.Sigma, equivalence_Elements, coyoneda]
+    congr! 1 with h
     . simp
-    . dsimp at h ⊢
-      rw! [h]
+    . rw! [← h]
       apply heq_of_eq
       ext : 1
       simp
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
index d5569d6..e0df980 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean
@@ -11,6 +11,11 @@ import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
 import Poly.ForMathlib.CategoryTheory.NatTrans
 import Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 
+-- Lean 4.34 tightened the transparency used by `simp`/`rw` when matching, so goals about
+-- `pullback.lift`/`pullback.fst` (reducible wrappers around `limit.lift`/`limit.π`) and about
+-- `Over.Hom` no longer close by `simp`. Mathlib's own `Over/Pullback.lean` sets the same option.
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 
 universe v₁ v₂ u₁ u₂
@@ -237,12 +242,12 @@ variable [HasBinaryProducts C]
 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]
+  simp
 
 @[simp]
 theorem counit_app {I : C} (X : C) :
-    ((forgetAdjStar I).counit.app X) = prod.snd := by
-  simp [Over.forgetAdjStar, Adjunction.comp, Equivalence.symm]
+    ((forgetAdjStar I).counit.app X) = prod.snd :=
+  forgetAdjStar_counit_app I X
 
 @[simp]
 theorem homEquiv_homMk_lift {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} :
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
index 609ffd6..e6c38a6 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean
@@ -16,6 +16,11 @@ of `X` over `I`.
 
 -/
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching, which breaks goals
+-- stated through reducible wrappers (`pullback.lift`/`pullback.fst`, `Over.Hom`).
+-- Mathlib sets the same option throughout its own `Over`/pullback files.
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 
 universe v₁ v₂ u₁ u₂
diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean
index b19ae69..761a435 100644
--- a/Poly/ForMathlib/CategoryTheory/Elements.lean
+++ b/Poly/ForMathlib/CategoryTheory/Elements.lean
@@ -15,7 +15,7 @@ variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟)
 @[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 (Subtype.mk (α := X ⟶ X) (𝟙 X) eq) = 𝟙 (G.obj (F.elementsMk X a)) :=
   show G.map (𝟙 _) = 𝟙 _ by simp
 
 @[simp]
diff --git a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
index e76ce64..0c7c0bc 100644
--- a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
@@ -22,9 +22,12 @@ 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
+  -- `IsPullback.cone`/`CommSq.cone` have no `pt` simp lemmas, so the cone points have to be
+  -- unfolded before `simp` can see through `𝟙 pb.cone.pt`.
+  apply WalkingCospan.ext j <;>
+    simp +zetaDelta [IsPullback.cone, CommSq.cone, PullbackCone.mk]
 
 end CategoryTheory.Functor
diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean
index ff77bff..00aa9fb 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean
@@ -46,6 +46,10 @@ in Mathematical Structures in Computer Science, 2024][Hazratpour_Riehl_2024]
 
 -/
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching, which breaks goals
+-- stated through reducible wrappers (`pullback.lift`/`pullback.fst`, `Over.Hom`).
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 namespace CategoryTheory
 
@@ -298,7 +302,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
 
@@ -312,7 +316,10 @@ theorem pullbackMapTwoSquare_app :
     Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by aesop) := by
   ext
   simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare]
-  aesop
+  apply pullback.hom_ext <;> simp
+  -- `𝟙` here sits at `((pullback f ⋙ map h).obj A).left`, which `simp` will not match
+  -- against `Limits.pullback A.hom f`; `exact` unifies them at default transparency.
+  exact Category.id_comp _
 
 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..d92734a 100644
--- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean
@@ -26,6 +26,10 @@ We construct a natural isomorphism
 `Over.map u ⋙ pushforward f ≅ pullback e ⋙ pushforward g ⋙  Over.map v`
 -/
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching, which breaks goals
+-- stated through reducible wrappers (`pullback.lift`/`pullback.fst`, `Over.Hom`).
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 namespace CategoryTheory
 
@@ -52,6 +56,10 @@ 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
 
+-- `PullbackCone.mk_pt` is not a `simp` lemma in mathlib, so cone points built with
+-- `PullbackCone.mk` do not reduce and `Category.id_comp` fails to match below.
+attribute [local simp] Limits.PullbackCone.mk_pt
+
 namespace ExponentiableMorphism
 
 def mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B)
@@ -62,6 +70,9 @@ def mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F :
   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
+  replace w : s.ι.left ≫ pullback.fst (X.hom ≫ F) F ≫ X.hom
+      = s.ι.left ≫ pullback.snd (X.hom ≫ F) F :=
+    w.trans (congrArg (fun t => s.ι.left ≫ t) (Category.id_comp _))
   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 ..)
diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
index e33d783..7cc66d2 100644
--- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
+++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean
@@ -17,6 +17,11 @@ with morphisms `fst : P —> A` and `snd : pullback fst s —> X`  which is univ
 such data.
 -/
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching, which breaks goals
+-- stated through reducible wrappers (`pullback.lift`/`pullback.fst`, `Over.Hom`).
+-- Mathlib sets the same option throughout its own `Over`/pullback files.
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 
 namespace CategoryTheory
diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean
index 3eb6659..2a2b35f 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
+  ConcreteCategory.congr_hom (NatTrans.congr_app (σ.naturality f) D₁) 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 ..
+  NatTrans.naturality_apply ..
 
 @[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/Type/Univariate.lean b/Poly/Type/Univariate.lean
index 0bb4cbe..592ad67 100644
--- a/Poly/Type/Univariate.lean
+++ b/Poly/Type/Univariate.lean
@@ -97,9 +97,7 @@ def sumTotalEquiv (P Q : Poly) : Total (sum P Q) ≃ Total P ⊕ Total Q where
   invFun := fun t => match t with
     | Sum.inl ⟨b, e⟩ => ⟨Sum.inl b, e⟩
     | Sum.inr ⟨c, f⟩ => ⟨Sum.inr c, f⟩
-  left_inv := by
-    simp
-    aesop_cat
+  left_inv := by rintro ⟨(b | c), e⟩ <;> rfl
   right_inv := by aesop_cat
 
 /-- The bundle associated to a polynomial `P`. -/
@@ -177,7 +175,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 := ↾(P.map f)
 
 variable {P}
 
@@ -189,7 +187,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 +222,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⟩ =>
-    ⟨ b.1, fun x' => ⟨ b.2 x', fun b' => e ⟨x',b'⟩ ⟩⟩
+    app := fun X => ↾(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 := ↾(comp.mk P Q)
     naturality := by aesop_cat
   }
 
diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean
index 74e0d4f..63c1f5e 100644
--- a/Poly/UvPoly/Basic.lean
+++ b/Poly/UvPoly/Basic.lean
@@ -33,6 +33,10 @@ in below.
 `Poly.Exponentiable`.
 -/
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching, which breaks goals
+-- stated through reducible wrappers (`pullback.lift`/`pullback.fst`, `Over.Hom`).
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 
 namespace CategoryTheory
@@ -137,7 +141,10 @@ def verticalNatTrans {F : C} (P : UvPoly E B) (Q : UvPoly F B) (ρ : E ⟶ F) (h
   let cellLeft := (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)))
+  -- `TwoSquare`, `UvPoly.functor` and `Over.star` are plain `def`s, so `simp` has to be told
+  -- to unfold them before the two sides line up.
+  simpa only [TwoSquare, UvPoly.functor, Over.star, Functor.assoc, Functor.comp_id] using
+    (cellLeftMidPasted ≫ₕ (vId (Over.forget B)))
 
 /-- A cartesian map of polynomials
 ```
@@ -309,7 +316,12 @@ def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct
     rw [← h_right]
     simp [forgetAdjStar, comp_homEquiv, Comonad.adj]
     simp [Equivalence.toAdjunction, homEquiv]
-    simp [coalgebraEquivOver, Equivalence.symm]; rfl
+    simp [coalgebraEquivOver, Equivalence.symm]
+    -- `simp` cannot match `Category.id_comp` here: the identity sits at
+    -- `((prodComonad E).cofree.obj X).A`, which is not syntactically the source of `prod.snd`.
+    rw [show 𝟙 ((prodComonad E).cofree.obj X).A ≫ (prod.snd : ((prodComonad E).cofree.obj X).A ⟶ X)
+        = prod.snd from Category.id_comp _]
+    rfl
 
 end PartialProduct
 
@@ -353,7 +365,7 @@ 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]
+  simp [proj, PartialProduct.Fan.extend]
 
 /-- 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) :=
diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean
index 4843fd9..d1bf926 100644
--- a/Poly/UvPoly/UPIso.lean
+++ b/Poly/UvPoly/UPIso.lean
@@ -6,6 +6,9 @@ Authors: Wojciech Nawrocki
 import Poly.UvPoly.Basic
 import Poly.Bifunctor.Sigma
 
+-- Lean 4.34 tightened the transparency `simp`/`rw` use when matching.
+set_option backward.isDefEq.respectTransparency false
+
 noncomputable section
 
 namespace CategoryTheory.UvPoly
@@ -25,13 +28,13 @@ 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 [partProdsOver, Functor.Sigma]
   have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp
-  ext : 1
+  refine Sigma.ext ?_ ?_
   . simp
   . dsimp
     rw! (castMode := .all) [this]
-    simp
+    simp [equivalence_Elements, pullback.lift_fst_snd]
 
 variable [HasTerminal C]
 
@@ -72,8 +75,8 @@ def equiv (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback
   Iso.toEquiv <| (P.iso_Sigma.app (.op Γ)).app X
 
 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]
+    P.equiv Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be :=
+  rfl
 
 lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) :
     P.equiv Δ X (σ ≫ be) =
diff --git a/lake-manifest.json b/lake-manifest.json
index f32e2f9..85dcfaa 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b8dad038b1b3a05b77d6884b15b8db03ec01dca1",
+   "rev": "85e3a25e006c35636f0e53b0e9296caca2685bc0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.34.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "ba67e212be1197b84c1f1f6299488a10a3002713",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
+   "rev": "d8823026ac7ef130c253089d95685f9877b95323",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f",
    "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": "18889deb9e83ea7420ef51c160d6f88552e744e3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "100083c18750b6a9b7553c65f6b052c0a2f6bcb4",
+   "rev": "d54dddc581e08be364c278052863524bff7a99a9",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,11 +95,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.34.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.lean b/lakefile.lean
index ae32354..8d3482e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -9,7 +9,7 @@ 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.0-rc2"
 
 @[default_target]
 lean_lib Poly where
@@ -19,4 +19,4 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.27.0-rc1"
+  "https://github.com/leanprover/doc-gen4" @ "v4.34.0-rc2"
diff --git a/lean-toolchain b/lean-toolchain
index 3e9b4e1..b814d98 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.0-rc2