chore: add @[ext] lemmas for NatTrans synonyms (#5228)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

@@ -49,17 +49,15 @@ def ringEquivEndForget₂ (R : Type u) [Ring R] :
   map_add' := by
     intros
     apply NatTrans.ext
-    ext1
-    dsimp
     ext
+    dsimp
     simp only [AddCommGroupCat.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, add_smul]
     rfl
   map_mul' := by
     intros
     apply NatTrans.ext
-    ext1
-    dsimp
     ext
+    dsimp
     simp only [AddCommGroupCat.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, mul_smul]
     rfl
 

Mathlib/AlgebraicGeometry/PresheafedSpace.lean

@@ -178,8 +178,7 @@ instance categoryOfPresheafedSpaces : Category (PresheafedSpace C) where
   id_comp _ := by
     dsimp
     ext
-    . apply NatTrans.ext
-      dsimp
+    . dsimp
       simp only [map_id, whiskerRight_id', assoc]
       erw [comp_id, comp_id]
     . dsimp
@@ -273,7 +272,7 @@ section Iso
 
 variable {X Y : PresheafedSpace C}
 
-/-- An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a
+/-- An isomorphism of `PresheafedSpace`s is a homeomorphism of the underlying space, and a
 natural transformation between the sheaves.
 -/
 @[simps hom inv]
@@ -286,8 +285,6 @@ def isoOfComponents (H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y wher
       c := Presheaf.toPushforwardOfIso H α.hom }
   hom_inv_id := by
     ext
-    apply NatTrans.ext
-    ext U
     rw [NatTrans.comp_app]
     simp only [id_base, comp_obj, op_obj, comp_base, Presheaf.pushforwardObj_obj,
       Opens.map_comp_obj, comp_c_app, unop_op, Presheaf.toPushforwardOfIso_app, assoc,
@@ -296,8 +293,6 @@ def isoOfComponents (H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y wher
     simp only [comp_base, Iso.hom_inv_id, FunctorToTypes.map_id_apply, id_base]
   inv_hom_id := by
     ext
-    apply NatTrans.ext
-    ext U
     dsimp
     rw [NatTrans.comp_app]
     simp only [Presheaf.pushforwardObj_obj, op_obj, Opens.map_comp_obj, comp_obj,
@@ -311,27 +306,25 @@ def isoOfComponents (H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y wher
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.iso_of_components AlgebraicGeometry.PresheafedSpace.isoOfComponents
 
-/-- Isomorphic PresheafedSpaces have naturally isomorphic presheaves. -/
+/-- Isomorphic `PresheafedSpace`s have naturally isomorphic presheaves. -/
 @[simps]
 def sheafIsoOfIso (H : X ≅ Y) : Y.2 ≅ H.hom.base _* X.2 where
   hom := H.hom.c
   inv := Presheaf.pushforwardToOfIso ((forget _).mapIso H).symm H.inv.c
   hom_inv_id := by
-    apply NatTrans.ext
     ext U
     rw [NatTrans.comp_app]
-    simpa using congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id U)
+    simpa using congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id (op U))
   inv_hom_id := by
-    apply NatTrans.ext
     ext U
     dsimp
     rw [NatTrans.comp_app, NatTrans.id_app]
     simp only [Presheaf.pushforwardObj_obj, op_obj, Presheaf.pushforwardToOfIso_app,
       Iso.symm_inv, mapIso_hom, forget_map, Iso.symm_hom, mapIso_inv,
       unop_op, eqToHom_map, assoc]
-    have eq₁ := congr_app H.hom_inv_id ((Opens.map H.hom.base).op.obj U)
+    have eq₁ := congr_app H.hom_inv_id (op ((Opens.map H.hom.base).obj U))
     have eq₂ := H.hom.c.naturality (eqToHom (congr_obj (congr_arg Opens.map
-      ((forget C).congr_map H.inv_hom_id.symm)) (Opposite.unop U))).op
+      ((forget C).congr_map H.inv_hom_id.symm)) U)).op
     rw [id_c, NatTrans.id_app, id_comp, eqToHom_map, comp_c_app] at eq₁
     rw [eqToHom_op, eqToHom_map] at eq₂
     erw [eq₂, reassoc_of% eq₁]
@@ -395,8 +388,7 @@ instance ofRestrict_mono {U : TopCat} (X : PresheafedSpace C) (f : U ⟶ X.1) (h
     simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
     rw [cancel_mono] at this
     exact this
-  . apply NatTrans.ext
-    ext ⟨V⟩
+  . ext V
     have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.isOpenMap.functor.obj V) = V := by
       ext1
       exact Set.preimage_image_eq _ hf.inj
@@ -438,8 +430,7 @@ theorem ofRestrict_top_c (X : PresheafedSpace C) :
   /- another approach would be to prove the left hand side
        is a natural isomorphism, but I encountered a universe
        issue when `apply NatIso.isIso_of_isIso_app`. -/
-  apply NatTrans.ext
-  ext1 U
+  ext
   dsimp [ofRestrict]
   erw [eqToHom_map, eqToHom_app]
   simp
@@ -527,15 +518,13 @@ def mapPresheaf (F : C ⥤ D) : PresheafedSpace C ⥤ PresheafedSpace D where
       c := whiskerRight f.c F }
   -- porting note: these proofs were automatic in mathlib3
   map_id X := by
-    -- Porting note: I don't understand why neither `ext` nor `aesop_cat` can apply `NatTrans.ext'`.
-    ext
-    apply NatTrans.ext'
-    aesop_cat
+    ext U
+    simp
+    rfl
   map_comp f g := by
-    -- Porting note: I don't understand why neither `ext` nor `aesop_cat` can apply `NatTrans.ext'`.
-    ext
-    apply NatTrans.ext'
-    aesop_cat
+    ext U
+    simp
+    rfl
 #align category_theory.functor.map_presheaf CategoryTheory.Functor.mapPresheaf
 
 @[simp]
@@ -573,12 +562,6 @@ def onPresheaf {F G : C ⥤ D} (α : F ⟶ G) : G.mapPresheaf ⟶ F.mapPresheaf
   app X :=
     { base := 𝟙 _
       c := whiskerLeft X.presheaf α ≫ eqToHom (Presheaf.Pushforward.id_eq _).symm }
-  -- porting note: this proof was automatic in mathlib3
-  naturality X Y f := by
-    -- Porting note: I don't understand why neither `ext` nor `aesop_cat` can apply `NatTrans.ext'`.
-    ext
-    apply NatTrans.ext
-    aesop_cat
 #align category_theory.nat_trans.on_presheaf CategoryTheory.NatTrans.onPresheaf
 
 -- TODO Assemble the last two constructions into a functor

Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -215,20 +215,18 @@ def colimitCocone (F : J ⥤ PresheafedSpace.{_, _, v} C) : Cocone F where
         fapply PresheafedSpace.ext
         · ext x
           exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x
-        · refine NatTrans.ext _ _ (funext fun U => ?_)
-          induction U with
-          | h U =>
-            rcases U with ⟨U, hU⟩
-            dsimp
-            rw [PresheafedSpace.id_c_app, map_id]
-            erw [id_comp]
-            rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app, eqToHom_app,
-              ← congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op),
-              NatTrans.comp_app, Functor.leftOp_map, pushforwardDiagramToColimit_map]
-            dsimp
-            rw [NatTrans.comp_app, NatTrans.comp_app, pushforwardEq_hom_app, id.def, eqToHom_op,
-              Pushforward.comp_inv_app, id_comp, pushforwardMap_app, ←assoc]
-            congr 1 }
+        · ext U
+          rcases U with ⟨U, hU⟩
+          dsimp
+          rw [PresheafedSpace.id_c_app, map_id]
+          erw [id_comp]
+          rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app, eqToHom_app,
+            ← congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op),
+            NatTrans.comp_app, Functor.leftOp_map, pushforwardDiagramToColimit_map]
+          dsimp
+          rw [NatTrans.comp_app, NatTrans.comp_app, pushforwardEq_hom_app, id.def, eqToHom_op,
+            Pushforward.comp_inv_app, id_comp, pushforwardMap_app, ←assoc]
+          congr 1 }
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.colimit_cocone AlgebraicGeometry.PresheafedSpace.colimitCocone
 
@@ -309,7 +307,7 @@ theorem desc_fac (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (j : J)
   · simp [desc]
   · -- Porting note : the original proof is just `ext; dsimp [desc, descCApp]; simpa`,
     -- but this has to be expanded a bit
-    refine NatTrans.ext _ _ (funext fun U => ?_)
+    ext U
     rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app]
     dsimp [desc, descCApp]
     simp only [eqToHom_app, op_obj, Opens.map_comp_obj, eqToHom_map, Functor.leftOp, assoc]

Mathlib/AlgebraicGeometry/Spec.lean

@@ -117,25 +117,24 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem Spec.sheafedSpaceMap_id {R : CommRingCat} :
     Spec.sheafedSpaceMap (𝟙 R) = 𝟙 (Spec.sheafedSpaceObj R) :=
-  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_id R) <|
-    NatTrans.ext _ _ <|
-      funext fun U => by
-        dsimp
-        erw [NatTrans.comp_app, sheafedSpaceMap_c_app, PresheafedSpace.id_c_app, comap_id]; swap
-        · rw [Spec.topMap_id, TopologicalSpace.Opens.map_id_obj_unop]
-        simp [eqToHom_map]
+  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_id R) <| by
+    ext U
+    dsimp
+    erw [NatTrans.comp_app, sheafedSpaceMap_c_app, PresheafedSpace.id_c_app, comap_id]; swap
+    · rw [Spec.topMap_id, TopologicalSpace.Opens.map_id_obj_unop]
+    simp [eqToHom_map]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.SheafedSpace_map_id AlgebraicGeometry.Spec.sheafedSpaceMap_id
 
 theorem Spec.sheafedSpaceMap_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) :
     Spec.sheafedSpaceMap (f ≫ g) = Spec.sheafedSpaceMap g ≫ Spec.sheafedSpaceMap f :=
-  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_comp f g) <|
-    NatTrans.ext _ _ <| funext fun U => by
-      -- Porting note : was one liner
-      -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
-      rw [NatTrans.comp_app, sheafedSpaceMap_c_app, whiskerRight_app, eqToHom_refl]
-      erw [(sheafedSpaceObj T).presheaf.map_id, Category.comp_id, comap_comp]
-      rfl
+  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_comp f g) <| by
+    ext
+    -- Porting note : was one liner
+    -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
+    rw [NatTrans.comp_app, sheafedSpaceMap_c_app, whiskerRight_app, eqToHom_refl]
+    erw [(sheafedSpaceObj T).presheaf.map_id, Category.comp_id, comap_comp]
+    rfl
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.SheafedSpace_map_comp AlgebraicGeometry.Spec.sheafedSpaceMap_comp
 
@@ -144,9 +143,9 @@ set_option linter.uppercaseLean3 false in
 @[simps]
 def Spec.toSheafedSpace : CommRingCatᵒᵖ ⥤ SheafedSpace CommRingCat where
   obj R := Spec.sheafedSpaceObj (unop R)
-  map {R S} f := Spec.sheafedSpaceMap f.unop
+  map f := Spec.sheafedSpaceMap f.unop
   map_id R := by dsimp; rw [Spec.sheafedSpaceMap_id]
-  map_comp {R S T} f g := by dsimp; rw [Spec.sheafedSpaceMap_comp]
+  map_comp f g := by dsimp; rw [Spec.sheafedSpaceMap_comp]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.to_SheafedSpace AlgebraicGeometry.Spec.toSheafedSpace
 
@@ -185,11 +184,10 @@ set_option linter.uppercaseLean3 false in
 
 theorem Spec.basicOpen_hom_ext {X : RingedSpace.{u}} {R : CommRingCat.{u}}
     {α β : X ⟶ Spec.sheafedSpaceObj R} (w : α.base = β.base)
-    (h :
-      ∀ r : R,
-        let U := PrimeSpectrum.basicOpen r
-        (toOpen R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom (by rw [w])) =
-          toOpen R U ≫ β.c.app (op U)) :
+    (h : ∀ r : R,
+      let U := PrimeSpectrum.basicOpen r
+      (toOpen R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom (by rw [w])) =
+        toOpen R U ≫ β.c.app (op U)) :
     α = β := by
   refine PresheafedSpace.ext (α := α) (β := β) w ?_
   · apply
@@ -295,9 +293,9 @@ set_option linter.uppercaseLean3 false in
 @[simps]
 def Spec.toLocallyRingedSpace : CommRingCatᵒᵖ ⥤ LocallyRingedSpace where
   obj R := Spec.locallyRingedSpaceObj (unop R)
-  map {R S} f := Spec.locallyRingedSpaceMap f.unop
+  map f := Spec.locallyRingedSpaceMap f.unop
   map_id R := by dsimp; rw [Spec.locallyRingedSpaceMap_id]
-  map_comp {R S T} f g := by dsimp; rw [Spec.locallyRingedSpaceMap_comp]
+  map_comp f g := by dsimp; rw [Spec.locallyRingedSpaceMap_comp]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.to_LocallyRingedSpace AlgebraicGeometry.Spec.toLocallyRingedSpace
 

Mathlib/AlgebraicGeometry/Stalks.lean

@@ -135,7 +135,7 @@ theorem id (X : PresheafedSpace.{_, _, v} C) (x : X) :
   simp only [stalkPushforward.id]
   erw [← map_comp]
   convert (stalkFunctor C x).map_id X.presheaf
-  refine NatTrans.ext _ _ <| funext fun x => ?_
+  ext
   simp only [id_c, id_comp, Pushforward.id_hom_app, op_obj, eqToHom_refl, map_id]
   rfl
 set_option linter.uppercaseLean3 false in

Mathlib/AlgebraicTopology/Nerve.lean

@@ -34,10 +34,6 @@ namespace CategoryTheory
 def nerve (C : Type u) [Category.{v} C] : SSet.{max u v} where
   obj Δ := SimplexCategory.toCat.obj Δ.unop ⥤ C
   map f x := SimplexCategory.toCat.map f.unop ⋙ x
-  map_id Δ := by
-    simp only [unop_id, id_eq]
-    ext x
-    apply Functor.id_comp
 #align category_theory.nerve CategoryTheory.nerve
 
 instance {C : Type _} [Category C] {Δ : SimplexCategoryᵒᵖ} : Category ((nerve C).obj Δ) :=
@@ -48,10 +44,6 @@ instance {C : Type _} [Category C] {Δ : SimplexCategoryᵒᵖ} : Category ((ner
 def nerveFunctor : Cat ⥤ SSet where
   obj C := nerve C
   map F := { app := fun Δ x => x ⋙ F }
-  map_id C := by
-    apply CategoryTheory.NatTrans.ext
-    funext Δ x
-    apply Functor.comp_id
 #align category_theory.nerve_functor CategoryTheory.nerveFunctor
 
 end CategoryTheory

Mathlib/AlgebraicTopology/SimplicialSet.lean

@@ -64,6 +64,12 @@ instance hasColimits : HasColimits SSet := by
   dsimp only [SSet]
   infer_instance
 
+-- Porting note: added an `ext` lemma.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
+@[ext]
+lemma hom_ext {X Y : SSet} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=
+  SimplicialObject.hom_ext _ _ w
+
 /-- The `n`-th standard simplex `Δ[n]` associated with a nonempty finite linear order `n`
 is the Yoneda embedding of `n`. -/
 def standardSimplex : SimplexCategory ⥤ SSet :=
@@ -129,8 +135,8 @@ set_option linter.uppercaseLean3 false in
 scoped[Simplicial] notation "Λ[" n ", " i "]" => SSet.horn (n : ℕ) i
 
 /-- The inclusion of the `i`-th horn of the `n`-th standard simplex into that standard simplex. -/
-def hornInclusion (n : ℕ) (i : Fin (n + 1)) : Λ[n, i] ⟶ Δ[n]
-    where app m (α : { α : Δ[n].obj m // _ }) := α
+def hornInclusion (n : ℕ) (i : Fin (n + 1)) : Λ[n, i] ⟶ Δ[n] where
+  app m (α : { α : Δ[n].obj m // _ }) := α
 set_option linter.uppercaseLean3 false in
 #align sSet.horn_inclusion SSet.hornInclusion
 
@@ -166,6 +172,12 @@ instance Truncated.hasColimits : HasColimits (Truncated n) := by
   dsimp only [Truncated]
   infer_instance
 
+-- Porting note: added an `ext` lemma.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
+@[ext]
+lemma Truncated.hom_ext {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=
+  NatTrans.ext _ _ (funext w)
+
 /-- The skeleton functor on simplicial sets. -/
 def sk (n : ℕ) : SSet ⥤ SSet.Truncated n :=
   SimplicialObject.sk n

Mathlib/CategoryTheory/Limits/FunctorCategory.lean

@@ -62,13 +62,12 @@ def evaluationJointlyReflectsLimits {F : J ⥤ K ⥤ C} (c : Cone F)
           rw [assoc, (t Y).fac _ j]
           simpa using
             ((t X).fac_assoc ⟨s.pt.obj X, whiskerRight s.π ((evaluation K C).obj X)⟩ j _).symm }
-  fac s j := NatTrans.ext _ _ <| funext fun k => (t k).fac _ j
-  uniq s m w :=
-    NatTrans.ext _ _ <|
-      funext fun x =>
-        (t x).hom_ext fun j =>
-          (congr_app (w j) x).trans
-            ((t x).fac ⟨s.pt.obj _, whiskerRight s.π ((evaluation K C).obj _)⟩ j).symm
+  fac s j := by ext k; exact (t k).fac _ j
+  uniq s m w := by
+    ext x
+    exact (t x).hom_ext fun j =>
+      (congr_app (w j) x).trans
+        ((t x).fac ⟨s.pt.obj _, whiskerRight s.π ((evaluation K C).obj _)⟩ j).symm
 #align category_theory.limits.evaluation_jointly_reflects_limits CategoryTheory.Limits.evaluationJointlyReflectsLimits
 
 /-- Given a functor `F` and a collection of limit cones for each diagram `X ↦ F X k`, we can stitch
@@ -89,7 +88,7 @@ def combineCones (F : J ⥤ K ⥤ C) (c : ∀ k : K, LimitCone (F.flip.obj k)) :
       map_comp := fun {k₁} {k₂} {k₃} f₁ f₂ => (c k₃).isLimit.hom_ext fun j => by simp }
   π :=
     { app := fun j => { app := fun k => (c k).cone.π.app j }
-      naturality := fun j₁ j₂ g => NatTrans.ext _ _ <| funext fun k => (c k).cone.π.naturality g }
+      naturality := fun j₁ j₂ g => by ext k; exact (c k).cone.π.naturality g }
 #align category_theory.limits.combine_cones CategoryTheory.Limits.combineCones
 
 /-- The stitched together cones each project down to the original given cones (up to iso). -/
@@ -121,13 +120,12 @@ def evaluationJointlyReflectsColimits {F : J ⥤ K ⥤ C} (c : Cocone F)
           erw [(t Y).fac ⟨s.pt.obj _, whiskerRight s.ι _⟩ j]
           dsimp
           simp }
-  fac s j := NatTrans.ext _ _ <| funext fun k => (t k).fac _ j
-  uniq s m w :=
-    NatTrans.ext _ _ <|
-      funext fun x =>
-        (t x).hom_ext fun j =>
-          (congr_app (w j) x).trans
-            ((t x).fac ⟨s.pt.obj _, whiskerRight s.ι ((evaluation K C).obj _)⟩ j).symm
+  fac s j := by ext k; exact (t k).fac _ j
+  uniq s m w := by
+    ext x
+    exact (t x).hom_ext fun j =>
+      (congr_app (w j) x).trans
+        ((t x).fac ⟨s.pt.obj _, whiskerRight s.ι ((evaluation K C).obj _)⟩ j).symm
 #align category_theory.limits.evaluation_jointly_reflects_colimits CategoryTheory.Limits.evaluationJointlyReflectsColimits
 
 /--
@@ -149,8 +147,7 @@ def combineCocones (F : J ⥤ K ⥤ C) (c : ∀ k : K, ColimitCocone (F.flip.obj
       map_comp := fun {k₁} {k₂} {k₃} f₁ f₂ => (c k₁).isColimit.hom_ext fun j => by simp }
   ι :=
     { app := fun j => { app := fun k => (c k).cocone.ι.app j }
-      naturality := fun j₁ j₂ g =>
-        NatTrans.ext _ _ <| funext fun k => (c k).cocone.ι.naturality g }
+      naturality := fun j₁ j₂ g => by ext k; exact (c k).cocone.ι.naturality g }
 #align category_theory.limits.combine_cocones CategoryTheory.Limits.combineCocones
 
 /-- The stitched together cocones each project down to the original given cocones (up to iso). -/