feat(CategoryTheory): use push attribute for CategoryTheory.inv. (leanprover-community#33820)

In this PR a few lemmas about isomorphisms are tagged `@[push]` or `@[push ←]`. The directionality of lemmas should be that the `inv` constant is pushed away from the head of the expression.

Some annotations are terminal, for instance, the ones for `inv (inv f) = f`, or `inv (e.hom) = e.inv` and `inv (e.inv) = e.hom`.

Running `push inv` thus normalizes inverses of expressions, though the form obtained is not necessarily the same as the simp normal form (simp normal forms in the library tend to "pull" the inverses outwards, while the push lemmas here are pushing them inwards).

These annotations will serve as building blocks for a simproc that cancels an isomorphism with its inverse within arbitrary nested expressions (functor compositions, whiskering in monoidal categories, natural isomorphisms of multifunctors, etc.). See leanprover-community#33822 for the implementation of the simproc, and how it uses the annotations introduced here.

Author: robin-carlier

Mathlib/CategoryTheory/Bicategory/Basic.lean

@@ -231,7 +231,7 @@ def whiskerLeftIso (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : f ≫ g ≅ f
 instance whiskerLeft_isIso (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] : IsIso (f ◁ η) :=
   (whiskerLeftIso f (asIso η)).isIso_hom
 
-@[simp]
+@[simp, push]
 theorem inv_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] :
     inv (f ◁ η) = f ◁ inv η := by
   apply IsIso.inv_eq_of_hom_inv_id
@@ -246,7 +246,7 @@ def whiskerRightIso {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : f ≫ h ≅ g
 instance whiskerRight_isIso {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] : IsIso (η ▷ h) :=
   (whiskerRightIso (asIso η) h).isIso_hom
 
-@[simp]
+@[simp, push]
 theorem inv_whiskerRight {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] :
     inv (η ▷ h) = inv η ▷ h := by
   apply IsIso.inv_eq_of_hom_inv_id

Mathlib/CategoryTheory/Comma/Basic.lean

@@ -180,12 +180,12 @@ instance [IsIso e] : IsIso e.left :=
 instance [IsIso e] : IsIso e.right :=
   (Comma.snd L R).map_isIso e
 
-@[simp]
+@[simp, push ←]
 lemma inv_left [IsIso e] : (inv e).left = inv e.left := by
   apply IsIso.eq_inv_of_hom_inv_id
   rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]
 
-@[simp]
+@[simp, push ←]
 lemma inv_right [IsIso e] : (inv e).right = inv e.right := by
   apply IsIso.eq_inv_of_hom_inv_id
   rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Mathlib/CategoryTheory/Iso.lean

@@ -358,22 +358,22 @@ theorem inv_id : inv (𝟙 X) = 𝟙 X := by
   apply inv_eq_of_hom_inv_id
   simp
 
-@[simp, reassoc]
+@[simp, reassoc, push]
 theorem inv_comp [IsIso f] [IsIso h] : inv (f ≫ h) = inv h ≫ inv f := by
   apply inv_eq_of_hom_inv_id
   simp
 
-@[simp]
+@[simp, push]
 theorem inv_inv [IsIso f] : inv (inv f) = f := by
   apply inv_eq_of_hom_inv_id
   simp
 
-@[simp]
+@[simp, push]
 theorem Iso.inv_inv (f : X ≅ Y) : inv f.inv = f.hom := by
   apply inv_eq_of_hom_inv_id
   simp
 
-@[simp]
+@[simp, push]
 theorem Iso.inv_hom (f : X ≅ Y) : inv f.hom = f.inv := by
   apply inv_eq_of_hom_inv_id
   simp
@@ -561,7 +561,7 @@ theorem mapIso_refl (F : C ⥤ D) (X : C) : F.mapIso (Iso.refl X) = Iso.refl (F.
 instance map_isIso (F : C ⥤ D) (f : X ⟶ Y) [IsIso f] : IsIso (F.map f) :=
   (F.mapIso (asIso f)).isIso_hom
 
-@[simp]
+@[simp, push ←]
 theorem map_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : F.map (inv f) = inv (F.map f) := by
   apply eq_inv_of_hom_inv_id
   simp [← F.map_comp]

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -357,7 +357,7 @@ def whiskerLeftIso (X : C) {Y Z : C} (f : Y ≅ Z) : X ⊗ Y ≅ X ⊗ Z where
 instance whiskerLeft_isIso (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] : IsIso (X ◁ f) :=
   (whiskerLeftIso X (asIso f)).isIso_hom
 
-@[simp]
+@[simp, push]
 theorem inv_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
     inv (X ◁ f) = X ◁ inv f := by
   cat_disch
@@ -385,7 +385,7 @@ def whiskerRightIso {X Y : C} (f : X ≅ Y) (Z : C) : X ⊗ Z ≅ Y ⊗ Z where
 instance whiskerRight_isIso {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] : IsIso (f ▷ Z) :=
   (whiskerRightIso (asIso f) Z).isIso_hom
 
-@[simp]
+@[simp, push]
 theorem inv_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] :
     inv (f ▷ Z) = inv f ▷ Z := by
   cat_disch
@@ -429,7 +429,7 @@ theorem tensorIso_def' {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
 instance tensor_isIso {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] : IsIso (f ⊗ₘ g) :=
   (asIso f ⊗ᵢ asIso g).isIso_hom
 
-@[simp]
+@[simp, push]
 theorem inv_tensor {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] :
     inv (f ⊗ₘ g) = inv f ⊗ₘ inv g := by
   simp [tensorHom_def, whisker_exchange]

Mathlib/CategoryTheory/NatIso.lean

@@ -176,8 +176,8 @@ theorem naturality_2' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app Y)} :
 instance isIso_app_of_isIso (α : F ⟶ G) [IsIso α] (X) : IsIso (α.app X) :=
   ⟨⟨(inv α).app X, ⟨by grind, by grind⟩⟩⟩
 
-@[simp]
-theorem isIso_inv_app (α : F ⟶ G) {_ : IsIso α} (X) : (inv α).app X = inv (α.app X) := by cat_disch
+@[simp, push ←]
+theorem isIso_inv_app (α : F ⟶ G) [IsIso α] (X) : (inv α).app X = inv (α.app X) := by cat_disch
 
 @[simp]
 theorem inv_map_inv_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :

Mathlib/CategoryTheory/Opposites.lean

@@ -174,12 +174,12 @@ theorem isIso_unop_iff {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsIso f.unop ↔ IsIso f
 instance isIso_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : IsIso f.unop :=
   (isIso_unop_iff _).2 inferInstance
 
-@[simp]
+@[simp, push ←]
 theorem op_inv {X Y : C} (f : X ⟶ Y) [IsIso f] : (inv f).op = inv f.op := by
   apply IsIso.eq_inv_of_hom_inv_id
   rw [← op_comp, IsIso.inv_hom_id, op_id]
 
-@[simp]
+@[simp, push ←]
 theorem unop_inv {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : (inv f).unop = inv f.unop := by
   apply IsIso.eq_inv_of_hom_inv_id
   rw [← unop_comp, IsIso.inv_hom_id, unop_id]