Sync upstream mathlib4 (2026-07-27, +5 commits)

Mathlib/CategoryTheory/Functor/Category.lean

@@ -150,7 +150,7 @@ end NatTrans
 namespace Functor
 
 /-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/
-@[simps (attr := grind =) obj_obj obj_map]
+@[implicit_reducible, simps (attr := grind =) obj_obj obj_map]
 protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
   obj k :=
     { obj := fun j => (F.obj j).obj k,
@@ -164,15 +164,15 @@ protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
 
 /-- The left unitor, a natural isomorphism `((𝟭 _) ⋙ F) ≅ F`.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def leftUnitor (F : C ⥤ D) :
     𝟭 C ⋙ F ≅ F where
   hom := { app := fun X => 𝟙 (F.obj X) }
   inv := { app := fun X => 𝟙 (F.obj X) }
 
 /-- The right unitor, a natural isomorphism `(F ⋙ (𝟭 B)) ≅ F`.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def rightUnitor (F : C ⥤ D) :
     F ⋙ 𝟭 D ≅ F where
   hom := { app := fun X => 𝟙 (F.obj X) }
@@ -183,7 +183,7 @@ def rightUnitor (F : C ⥤ D) :
 (In fact, `iso.refl _` will work here, but it tends to make Lean slow later,
 and it's usually best to insert explicit associators.)
 -/
-@[simps]
+@[implicit_reducible, simps]
 def associator (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') :
     (F ⋙ G) ⋙ H ≅ F ⋙ G ⋙ H where
   hom := { app := fun _ => 𝟙 _ }
@@ -196,7 +196,7 @@ end Functor
 
 variable (C D E) in
 /-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/
-@[simps]
+@[implicit_reducible, simps]
 def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where
   obj F := F.flip
   map {F₁ F₂} φ :=

Mathlib/CategoryTheory/Functor/Currying.lean

@@ -54,6 +54,7 @@ def uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E where
 
 /-- The object level part of the currying functor. (See `curry` for the functorial version.)
 -/
+@[implicit_reducible]
 def curryObj (F : C × D ⥤ E) : C ⥤ D ⥤ E where
   obj X :=
     { obj := fun Y => F.obj (X, Y)
@@ -68,7 +69,7 @@ def curryObj (F : C × D ⥤ E) : C ⥤ D ⥤ E where
 
 /-- The currying functor, taking a functor `(C × D) ⥤ E` and producing a functor `C ⥤ (D ⥤ E)`.
 -/
-@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
+@[implicit_reducible, simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
 def curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E where
   obj F := curryObj F
   map T :=
@@ -81,12 +82,10 @@ def curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E where
         ext; dsimp [curryObj]
         rw [NatTrans.naturality] }
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 -- create projection simp lemmas even though this isn't a `{ .. }`.
 /-- The equivalence of functor categories given by currying/uncurrying.
 -/
-@[simps!]
+@[implicit_reducible, simps!]
 def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where
   functor := uncurry
   inverse := curry
@@ -98,10 +97,8 @@ def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where
       dsimp at f₁ f₂ ⊢
       simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp]))
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The equivalence of functor categories given by flipping. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flipping : C ⥤ D ⥤ E ≌ D ⥤ C ⥤ E where
   functor := flipFunctor _ _ _
   inverse := flipFunctor _ _ _
@@ -132,8 +129,6 @@ instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Full :=
 instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Faithful :=
   fullyFaithfulUncurry.faithful
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- Given functors `F₁ : C ⥤ D`, `F₂ : C' ⥤ D'` and `G : D × D' ⥤ E`, this is the isomorphism
 between `curry.obj ((F₁.prod F₂).comp G)` and
 `F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂` in the category `C ⥤ C' ⥤ E`. -/
@@ -144,37 +139,29 @@ def curryObjProdComp {C' D' : Type*} [Category* C'] [Category* D']
       F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ :=
   NatIso.ofComponents (fun X₁ ↦ NatIso.ofComponents (fun X₂ ↦ Iso.refl _))
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flipIsoCurrySwapUncurry (F : C ⥤ D ⥤ E) : F.flip ≅ curry.obj (Prod.swap _ _ ⋙ uncurry.obj F) :=
   NatIso.ofComponents fun d => NatIso.ofComponents fun _ => Iso.refl _
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The uncurrying of `F.flip` is isomorphic to
 swapping the factors followed by the uncurrying of `F`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def uncurryObjFlip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ Prod.swap _ _ ⋙ uncurry.obj F :=
   NatIso.ofComponents fun _ => Iso.refl _
 
 variable (B C D E)
 
-#adaptation_note
-/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/
-set_option backward.isDefEq.respectTransparency.types false in
 /-- A version of `CategoryTheory.whiskeringRight` for bifunctors, obtained by uncurrying,
 applying `whiskeringRight` and currying back
 -/
-@[simps!]
+@[implicit_reducible, simps!]
 def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E :=
   uncurry ⋙
     whiskeringRight _ _ _ ⋙ (whiskeringLeft _ _ _).obj (prodFunctorToFunctorProd _ _ _) ⋙ curry
 
 variable {B C D E}
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma uncurry_obj_curry_obj (F : B × C ⥤ D) : uncurry.obj (curry.obj F) = F :=
   Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
     dsimp
@@ -184,8 +171,6 @@ lemma curry_obj_injective {F₁ F₂ : C × D ⥤ E} (h : curry.obj F₁ = curry
     F₁ = F₂ := by
   rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma curry_obj_uncurry_obj (F : B ⥤ C ⥤ D) : curry.obj (uncurry.obj F) = F :=
   Functor.ext (fun _ => Functor.ext (by simp) (by simp)) (by cat_disch)
 
@@ -199,32 +184,28 @@ lemma flip_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : F₁.flip = F₂.flip) :
     F₁ = F₂ := by
   rw [← flip_flip F₁, ← flip_flip F₂, h]
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma uncurry_obj_curry_obj_flip_flip (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
     uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip = (F₁.prod F₂) ⋙ G :=
   Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
     dsimp
     simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma uncurry_obj_curry_obj_flip_flip' (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
     uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip) = (F₁.prod F₂) ⋙ G :=
   Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
     dsimp
     simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])
 
 /-- Natural isomorphism witnessing `comp_flip_uncurry_eq`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def compFlipUncurryIso (F : B ⥤ D) (G : D ⥤ C ⥤ E) :
     uncurry.obj (F ⋙ G).flip ≅ (𝟭 C).prod F ⋙ uncurry.obj G.flip := .refl _
 
 lemma comp_flip_uncurry_eq (F : B ⥤ D) (G : D ⥤ C ⥤ E) :
     uncurry.obj (F ⋙ G).flip = (𝟭 C).prod F ⋙ uncurry.obj G.flip := rfl
 
 /-- Natural isomorphism witnessing `comp_flip_curry_eq`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def curryObjCompIso (F : C × B ⥤ D) (G : D ⥤ E) :
     (curry.obj (F ⋙ G)).flip ≅ (curry.obj F).flip ⋙ (whiskeringRight _ _ _).obj G := .refl _
 
@@ -233,23 +214,23 @@ lemma curry_obj_comp_flip (F : C × B ⥤ D) (G : D ⥤ E) :
       (curry.obj F).flip ⋙ (whiskeringRight _ _ _).obj G := rfl
 
 /-- The equivalence of types of bifunctors giving by flipping the arguments. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flippingEquiv : C ⥤ D ⥤ E ≃ D ⥤ C ⥤ E where
   toFun F := F.flip
   invFun F := F.flip
   left_inv _ := rfl
   right_inv _ := rfl
 
 /-- The equivalence of types of bifunctors given by currying. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def curryingEquiv : C ⥤ D ⥤ E ≃ C × D ⥤ E where
   toFun F := uncurry.obj F
   invFun G := curry.obj G
   left_inv := curry_obj_uncurry_obj
   right_inv := uncurry_obj_curry_obj
 
 /-- The flipped equivalence of types of bifunctors given by currying. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def curryingFlipEquiv : D ⥤ C ⥤ E ≃ C × D ⥤ E :=
   flippingEquiv.trans curryingEquiv
 

Mathlib/CategoryTheory/Iso.lean

@@ -83,7 +83,7 @@ theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
     _     = β.inv                 := by grind
 
 /-- Inverse isomorphism. -/
-@[symm]
+@[symm, implicit_reducible]
 def symm (I : X ≅ Y) : Y ≅ X where
   hom := I.inv
   inv := I.hom
@@ -112,7 +112,7 @@ theorem nonempty_iso_symm (X Y : C) : Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)
   ⟨fun h => ⟨h.some.symm⟩, fun h => ⟨h.some.symm⟩⟩
 
 /-- Identity isomorphism. -/
-@[refl, simps (attr := grind =)]
+@[refl, simps (attr := grind =), implicit_reducible]
 def refl (X : C) : X ≅ X where
   hom := 𝟙 X
   inv := 𝟙 X
@@ -127,7 +127,7 @@ theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩
 theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl
 
 /-- Composition of two isomorphisms -/
-@[simps (attr := grind =)]
+@[simps (attr := grind =), implicit_reducible]
 def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
   hom := α.hom ≫ β.hom
   inv := β.inv ≫ α.inv
@@ -219,7 +219,7 @@ theorem hom_eq_inv (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom =
 attribute [local grind] Function.LeftInverse Function.RightInverse
 
 /-- The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`. -/
-@[to_dual (attr := simps) homFromEquiv
+@[implicit_reducible, to_dual (attr := simps) homFromEquiv
 /-- The bijection `(X ⟶ Z) ≃ (Y ⟶ Z)` induced by `α : X ≅ Y`. -/]
 def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where
   toFun f := f ≫ α.hom
@@ -469,7 +469,7 @@ variable {D : Type u₂}
 variable [Category.{v₂} D]
 
 /-- A functor `F : C ⥤ D` sends isomorphisms `i : X ≅ Y` to isomorphisms `F.obj X ≅ F.obj Y` -/
-@[simps]
+@[simps, implicit_reducible]
 def mapIso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y where
   hom := F.map i.hom
   inv := F.map i.inv

Mathlib/CategoryTheory/NatIso.lean

@@ -176,7 +176,7 @@ set_option linter.translate.warnInvalid false in
 /-- Construct a natural isomorphism between functors by giving object level isomorphisms,
 and checking naturality only in the forward direction.
 -/
-@[to_dual (attr := simps (attr := grind =)) ofComponents'
+@[implicit_reducible, to_dual (attr := simps (attr := grind =)) ofComponents'
 /-- The dual of `ofComponents` -/]
 def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X)
     (naturality : ∀ {X Y : C} (f : X ⟶ Y),

Mathlib/CategoryTheory/Preadditive/Projective/Preserves.lean

@@ -12,7 +12,7 @@ public import Mathlib.CategoryTheory.Preadditive.Projective.Basic
 
 We define a typeclass `Functor.PreservesProjectiveObjects`.
 
-We restate the existing result that if `F ⊣ G` is an adjunction and `G` preserves monomorphisms,
+We restate the existing result that if `F ⊣ G` is an adjunction and `G` preserves epimorphisms,
 then `F` preserves projective objects. We show that the converse is true if the domain of `F` has
 enough projectives.
 -/