feat(CategoryTheory/NatTrans): use to_dual (#33834)

This PR tags `NatTrans` with `to_dual`. The two functor arguments get swapped because the underlying `NatTrans.app` has its direction swapped.

Translating the `naturality` field is slightly awkward. We need to define a constant `naturality'` (analogously to `Category.assoc')

Author: JovanGerb

Mathlib/CategoryTheory/NatTrans.lean

@@ -48,19 +48,25 @@ The field `app` provides the components of the natural transformation.
 
 Naturality is expressed by `α.naturality`.
 -/
-@[ext]
+@[ext, to_dual self (reorder := F G)]
 structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
   /-- The component of a natural transformation. -/
-  app : ∀ X : C, F.obj X ⟶ G.obj X
+  app (X : C) : F.obj X ⟶ G.obj X
   /-- The naturality square for a given morphism. -/
-  naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f := by cat_disch
+  naturality ⦃X Y : C⦄ (f : X ⟶ Y) : F.map f ≫ app Y = app X ≫ G.map f := by cat_disch
+
+set_option linter.translateOverwrite false in
+@[to_dual existing naturality]
+lemma NatTrans.naturality' {F G : C ⥤ D} (self : NatTrans G F) ⦃X Y : C⦄ (f : Y ⟶ X) :
+    self.app Y ≫ F.map f = G.map f ≫ self.app X := (self.naturality f).symm
 
 -- Rather arbitrarily, we say that the 'simpler' form is
 -- components of natural transformations moving earlier.
 attribute [reassoc (attr := simp)] NatTrans.naturality
 
 attribute [grind _=_] NatTrans.naturality
 
+@[to_dual self]
 theorem congr_app {F G : C ⥤ D} {α β : NatTrans F G} (h : α = β) (X : C) : α.app X = β.app X := by
   cat_disch
 
@@ -83,11 +89,13 @@ section
 variable {F G H : C ⥤ D}
 
 /-- `vcomp α β` is the vertical compositions of natural transformations. -/
+@[to_dual self (reorder := F H, α β)]
 def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where
   app X := α.app X ≫ β.app X
 
 -- functor_category will rewrite (vcomp α β) to (α ≫ β), so this is not a
 -- suitable simp lemma.  We will declare the variant vcomp_app' there.
+@[to_dual self]
 theorem vcomp_app (α : NatTrans F G) (β : NatTrans G H) (X : C) :
     (vcomp α β).app X = α.app X ≫ β.app X := rfl