feat: use grind in CategoryTheory.NatIso

Author: kim-em

Mathlib/CategoryTheory/Functor/Category.lean

@@ -57,7 +57,7 @@ instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where
 
 namespace NatTrans
 
-@[ext]
+@[ext, grind ext]
 theorem ext' {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w
 
 @[simp]

Mathlib/CategoryTheory/Iso.lean

@@ -66,40 +66,34 @@ variable {C : Type u} [Category.{v} C] {X Y Z : C}
 
 namespace Iso
 
-@[ext]
+@[ext, grind ext]
 theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
-  suffices α.inv = β.inv by
-    cases α
-    cases β
-    cases w
-    cases this
-    rfl
+  suffices α.inv = β.inv by grind [Iso]
   calc
-    α.inv = α.inv ≫ β.hom ≫ β.inv   := by grind
-    _     = (α.inv ≫ α.hom) ≫ β.inv := by grind
-    _     = β.inv                    := by grind
+    α.inv = α.inv ≫ β.hom ≫ β.inv := by grind
+    _     = β.inv                 := by grind
 
 /-- Inverse isomorphism. -/
 @[symm]
 def symm (I : X ≅ Y) : Y ≅ X where
   hom := I.inv
   inv := I.hom
 
-@[simp]
+@[simp, grind =]
 theorem symm_hom (α : X ≅ Y) : α.symm.hom = α.inv :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem symm_inv (α : X ≅ Y) : α.symm.inv = α.hom :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem symm_mk {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) :
     Iso.symm { hom, inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } =
       { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id } :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem symm_symm_eq {X Y : C} (α : X ≅ Y) : α.symm.symm = α := rfl
 
 theorem symm_bijective {X Y : C} : Function.Bijective (symm : (X ≅ Y) → _) :=
@@ -118,11 +112,13 @@ def refl (X : C) : X ≅ X where
   hom := 𝟙 X
   inv := 𝟙 X
 
+attribute [grind =] refl_hom refl_inv
+
 instance : Inhabited (X ≅ X) := ⟨Iso.refl X⟩
 
 theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩
 
-@[simp]
+@[simp, grind =]
 theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl
 
 /-- Composition of two isomorphisms -/
@@ -131,25 +127,27 @@ def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
   hom := α.hom ≫ β.hom
   inv := β.inv ≫ α.inv
 
+attribute [grind =] trans_hom trans_inv
+
 @[simps]
 instance instTransIso : Trans (α := C) (· ≅ ·) (· ≅ ·) (· ≅ ·) where
   trans := trans
 
 /-- Notation for composition of isomorphisms. -/
 infixr:80 " ≪≫ " => Iso.trans -- type as `\ll \gg`.
 
-@[simp]
+@[simp, grind =]
 theorem trans_mk {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id)
     (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id') (inv_hom_id') (hom_inv_id'') (inv_hom_id'') :
     Iso.trans ⟨hom, inv, hom_inv_id, inv_hom_id⟩ ⟨hom', inv', hom_inv_id', inv_hom_id'⟩ =
      ⟨hom ≫ hom', inv' ≫ inv, hom_inv_id'', inv_hom_id''⟩ :=
   rfl
 
-@[simp]
+@[simp, grind _=_]
 theorem trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).symm = β.symm ≪≫ α.symm :=
   rfl
 
-@[simp]
+@[simp, grind _=_]
 theorem trans_assoc {Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') :
     (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ := by
   ext; simp only [trans_hom, Category.assoc]
@@ -240,11 +238,11 @@ noncomputable def inv (f : X ⟶ Y) [I : IsIso f] : Y ⟶ X :=
 
 namespace IsIso
 
-@[simp]
+@[simp, grind =]
 theorem hom_inv_id (f : X ⟶ Y) [I : IsIso f] : f ≫ inv f = 𝟙 X :=
   (Classical.choose_spec I.1).left
 
-@[simp]
+@[simp, grind =]
 theorem inv_hom_id (f : X ⟶ Y) [I : IsIso f] : inv f ≫ f = 𝟙 Y :=
   (Classical.choose_spec I.1).right
 
@@ -269,7 +267,7 @@ theorem inv_hom_id_assoc (f : X ⟶ Y) [I : IsIso f] {Z} (g : Y ⟶ Z) : inv f 
 end IsIso
 
 lemma Iso.isIso_hom (e : X ≅ Y) : IsIso e.hom :=
-  ⟨e.inv, by simp, by simp⟩
+  ⟨e.inv, by simp only [hom_inv_id], by simp⟩
 
 lemma Iso.isIso_inv (e : X ≅ Y) : IsIso e.inv := e.symm.isIso_hom
 
@@ -308,16 +306,16 @@ instance (priority := 100) mono_of_iso (f : X ⟶ Y) [IsIso f] : Mono f where
     rw [← Category.comp_id g, ← Category.comp_id h, ← IsIso.hom_inv_id f,
       ← Category.assoc, w, ← Category.assoc]
 
-@[aesop apply safe (rule_sets := [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory]), grind ←=]
 theorem inv_eq_of_hom_inv_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :
     inv f = g := by
-  apply (cancel_epi f).mp
-  simp [hom_inv_id]
+  have := congrArg (inv f ≫ ·) hom_inv_id
+  grind
 
 theorem inv_eq_of_inv_hom_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) :
     inv f = g := by
-  apply (cancel_mono f).mp
-  simp [inv_hom_id]
+  have := congrArg (· ≫ inv f) inv_hom_id
+  grind
 
 @[aesop apply safe (rule_sets := [CategoryTheory])]
 theorem eq_inv_of_hom_inv_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :
@@ -503,15 +501,13 @@ section
 
 variable {D : Type*} [Category D] {X Y : C} (e : X ≅ Y)
 
-@[reassoc (attr := simp), grind =]
+@[reassoc (attr := simp)]
 lemma map_hom_inv_id (F : C ⥤ D) :
-    F.map e.hom ≫ F.map e.inv = 𝟙 _ := by
-  rw [← F.map_comp, e.hom_inv_id, F.map_id]
+    F.map e.hom ≫ F.map e.inv = 𝟙 _ := by grind
 
-@[reassoc (attr := simp), grind =]
+@[reassoc (attr := simp)]
 lemma map_inv_hom_id (F : C ⥤ D) :
-    F.map e.inv ≫ F.map e.hom = 𝟙 _ := by
-  rw [← F.map_comp, e.inv_hom_id, F.map_id]
+    F.map e.inv ≫ F.map e.hom = 𝟙 _ := by grind
 
 end
 

Mathlib/CategoryTheory/NatIso.lean

@@ -30,6 +30,8 @@ we put some declarations that are specifically about natural isomorphisms in the
 namespace so that they are available using dot notation.
 -/
 
+set_option mathlib.tactic.category.grind true
+
 -- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
 universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
 
@@ -49,44 +51,34 @@ def app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
     F.obj X ≅ G.obj X where
   hom := α.hom.app X
   inv := α.inv.app X
-  hom_inv_id := by rw [← comp_app, Iso.hom_inv_id]; rfl
-  inv_hom_id := by rw [← comp_app, Iso.inv_hom_id]; rfl
 
 attribute [grind =] app_hom app_inv
 
 @[reassoc (attr := simp), grind =]
 theorem hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
-    α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
-  congr_fun (congr_arg NatTrans.app α.hom_inv_id) X
+    α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) := by cat_disch
 
 @[reassoc (attr := simp), grind =]
 theorem inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
-    α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
-  congr_fun (congr_arg NatTrans.app α.inv_hom_id) X
+    α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) := by cat_disch
 
 @[reassoc (attr := simp)]
 lemma hom_inv_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
-    (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _ := by
-  rw [← NatTrans.comp_app, Iso.hom_inv_id_app, NatTrans.id_app]
+    (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _ := by cat_disch
 
 @[reassoc (attr := simp)]
 lemma inv_hom_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
-    (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _ := by
-  rw [← NatTrans.comp_app, Iso.inv_hom_id_app, NatTrans.id_app]
+    (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _ := by cat_disch
 
 @[reassoc (attr := simp)]
 lemma hom_inv_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G)
     (X₁ : C) (X₂ : D) (X₃ : E) :
-    ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 _ := by
-  rw [← NatTrans.comp_app, ← NatTrans.comp_app, Iso.hom_inv_id_app,
-    NatTrans.id_app, NatTrans.id_app]
+    ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 _ := by cat_disch
 
 @[reassoc (attr := simp)]
 lemma inv_hom_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G)
     (X₁ : C) (X₂ : D) (X₃ : E) :
-    ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 _ := by
-  rw [← NatTrans.comp_app, ← NatTrans.comp_app, Iso.inv_hom_id_app,
-    NatTrans.id_app, NatTrans.id_app]
+    ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 _ := by cat_disch
 
 end Iso
 
@@ -110,12 +102,10 @@ theorem app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv
 variable {F G : C ⥤ D}
 
 instance hom_app_isIso (α : F ≅ G) (X : C) : IsIso (α.hom.app X) :=
-  ⟨⟨α.inv.app X,
-    ⟨by rw [← comp_app, Iso.hom_inv_id, ← id_app], by rw [← comp_app, Iso.inv_hom_id, ← id_app]⟩⟩⟩
+  ⟨⟨α.inv.app X, ⟨by grind, by grind⟩⟩⟩
 
 instance inv_app_isIso (α : F ≅ G) (X : C) : IsIso (α.inv.app X) :=
-  ⟨⟨α.hom.app X,
-    ⟨by rw [← comp_app, Iso.inv_hom_id, ← id_app], by rw [← comp_app, Iso.hom_inv_id, ← id_app]⟩⟩⟩
+  ⟨⟨α.hom.app X, ⟨by grind, by grind⟩⟩⟩
 
 section
 
@@ -161,8 +151,6 @@ theorem cancel_natIso_inv_right_assoc {W X X' : D} {Y : C} (f : W ⟶ X) (g : X
     f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g' := by
   simp only [← Category.assoc, cancel_mono, refl]
 
-attribute [grind ←=] CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-
 @[simp]
 theorem inv_inv_app {F G : C ⥤ D} (e : F ≅ G) (X : C) : inv (e.inv.app X) = e.hom.app X := by
   cat_disch
@@ -182,30 +170,24 @@ theorem naturality_1' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app X)} :
 
 @[reassoc (attr := simp)]
 theorem naturality_2' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app Y)} :
-    α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f := by
-  rw [← Category.assoc, ← naturality, Category.assoc, IsIso.hom_inv_id, Category.comp_id]
+    α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f := by cat_disch
 
 /-- The components of a natural isomorphism are isomorphisms.
 -/
 instance isIso_app_of_isIso (α : F ⟶ G) [IsIso α] (X) : IsIso (α.app X) :=
-  ⟨⟨(inv α).app X,
-      ⟨congr_fun (congr_arg NatTrans.app (IsIso.hom_inv_id α)) X,
-        congr_fun (congr_arg NatTrans.app (IsIso.inv_hom_id α)) X⟩⟩⟩
+  ⟨⟨(inv α).app X, ⟨by grind, by grind⟩⟩⟩
 
 @[simp]
-theorem isIso_inv_app (α : F ⟶ G) {_ : IsIso α} (X) : (inv α).app X = inv (α.app X) := by
-  -- Porting note: the next lemma used to be in `ext`, but that is no longer allowed.
-  -- We've added an aesop apply rule;
-  -- it would be nice to have a hook to run those without aesop warning it didn't close the goal.
-  apply IsIso.eq_inv_of_hom_inv_id
-  rw [← NatTrans.comp_app]
-  simp
+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) :
-    inv ((F.map e.inv).app Z) = (F.map e.hom).app Z := by
-  cat_disch
+    inv ((F.map e.inv).app Z) = (F.map e.hom).app Z := by cat_disch
 
+-- TODO: `hom_inv_id` and `inv_hom_id` are not yet working via `grind`,
+-- but they work fine in my minimization in the `grind` test suite.
+-- Investigate on nightly-testing / the next release?
+set_option mathlib.tactic.category.grind false in
 /-- Construct a natural isomorphism between functors by giving object level isomorphisms,
 and checking naturality only in the forward direction.
 -/
@@ -222,9 +204,11 @@ def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X)
         simp only [Iso.inv_hom_id_assoc, Iso.hom_inv_id, assoc, comp_id] at h
         exact h }
 
+attribute [grind =] ofComponents_hom_app ofComponents_inv_app
+
 @[simp]
 theorem ofComponents.app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
-    (ofComponents app' naturality).app X = app' X := by aesop
+    (ofComponents app' naturality).app X = app' X := by cat_disch
 
 -- Making this an instance would cause a typeclass inference loop with `isIso_app_of_isIso`.
 /-- A natural transformation is an isomorphism if all its components are isomorphisms.
@@ -234,22 +218,17 @@ theorem isIso_of_isIso_app (α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso
 
 /-- Horizontal composition of natural isomorphisms. -/
 @[simps]
-def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I := by
-  refine ⟨α.hom ◫ β.hom, α.inv ◫ β.inv, ?_, ?_⟩
-  · ext
-    rw [← NatTrans.exchange]
-    simp
-  ext; rw [← NatTrans.exchange]; simp
+def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I where
+  hom := α.hom ◫ β.hom
+  inv := α.inv ◫ β.inv
 
 theorem isIso_map_iff {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) :
     IsIso (F₁.map f) ↔ IsIso (F₂.map f) := by
   revert F₁ F₂
-  suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) by
-    exact fun F₁ F₂ e => ⟨this e, this e.symm⟩
+  suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from
+    fun F₁ F₂ e => ⟨this e, this e.symm⟩
   intro F₁ F₂ e hf
-  refine IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, ?_, ?_⟩
-  · simp only [NatTrans.naturality_assoc, IsIso.hom_inv_id_assoc, Iso.inv_hom_id_app]
-  · simp only [assoc, ← e.hom.naturality, IsIso.inv_hom_id_assoc, Iso.inv_hom_id_app]
+  exact IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, by cat_disch⟩
 
 end NatIso
 
@@ -261,6 +240,7 @@ namespace Functor
 
 variable (F : C ⥤ D) (obj : C → D) (e : ∀ X, F.obj X ≅ obj X)
 
+set_option mathlib.tactic.category.grind false in
 /-- Constructor for a functor that is isomorphic to a given functor `F : C ⥤ D`,
 while being definitionally equal on objects to a given map `obj : C → D`
 such that for all `X : C`, we have an isomorphism `F.obj X ≅ obj X`. -/