.

Author: kim-em

Mathlib/CategoryTheory/Functor/Basic.lean

@@ -18,6 +18,7 @@ from `C` to `D`, `𝟭` for the identity functor and `⋙` for functor compositi
 TODO: Switch to using the `⇒` arrow.
 -/
 
+set_option mathlib.tactic.category.grind true
 
 namespace CategoryTheory
 

Mathlib/CategoryTheory/HomCongr.lean

@@ -22,6 +22,8 @@ which can be found in  `CategoryTheory.Conj`.
 -/
 
 
+set_option mathlib.tactic.category.grind true
+
 universe v u
 
 namespace CategoryTheory

Mathlib/CategoryTheory/Iso.lean

@@ -31,6 +31,8 @@ This file defines isomorphisms between objects of a category.
 category, category theory, isomorphism
 -/
 
+set_option mathlib.tactic.category.grind true
+
 universe v u
 
 -- morphism levels before object levels. See note [CategoryTheory universes].

Mathlib/CategoryTheory/NatTrans.lean

@@ -29,6 +29,8 @@ Introduces notations
 
 -/
 
+set_option mathlib.tactic.category.grind true
+
 namespace CategoryTheory
 
 -- declare the `v`'s first; see note [CategoryTheory universes].