chore: bump to v4.34.0-rc2

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

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

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} :

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₂

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]

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

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) =

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 ..)

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

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

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
   }