feat: add Aesop rules for Discrete category (#2519)

Adds a global Aesop `cases` rule for the `Discrete` category. This rule was previously added locally in several places.
leanprover-community · Jun 21, 2023 · ecb36a8 · ecb36a8
1 parent e032d37
commit ecb36a8
Show file tree

Hide file tree

Showing 11 changed files with 1 addition and 23 deletions.
diff --git a/Mathlib/CategoryTheory/Adjunction/Comma.lean b/Mathlib/CategoryTheory/Adjunction/Comma.lean
@@ -141,8 +141,6 @@ section
 
 variable {F : C ⥤ D}
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- Given a left adjoint to `G`, we can construct an initial object in each structured arrow
 category on `G`. -/
 def mkInitialOfLeftAdjoint (h : F ⊣ G) (A : C) :

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -47,7 +47,7 @@ universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
 /-- A wrapper for promoting any type to a category,
 with the only morphisms being equalities.
 -/
-@[ext]
+@[ext, aesop safe cases (rule_sets [CategoryTheory])]
 structure Discrete (α : Type u₁) where
   /-- A wrapper for promoting any type to a category,
   with the only morphisms being equalities. -/

diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean
@@ -196,8 +196,6 @@ variable [HasCoproducts.{0} C]
 
 section
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- The total object of a graded object is the coproduct of the graded components.
 -/
 noncomputable def total : GradedObject β C ⥤ C where

diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean
@@ -165,8 +165,6 @@ theorem over_finiteProducts_of_finiteWidePullbacks [HasFiniteWidePullbacks C] {B
 
 end ConstructProducts
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- Construct terminal object in the over category. This isn't an instance as it's not typically the
 way we want to define terminal objects.
 (For instance, this gives a terminal object which is different from the generic one given by

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -52,8 +52,6 @@ variable {C : Type u} [Category.{v} C]
 -- We don't need an analogue of `Pair` (for binary products), `ParallelPair` (for equalizers),
 -- or `(Co)span`, since we already have `Discrete.functor`.
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`. -/
 abbrev Fan (f : β → C) :=
   Cone (Discrete.functor f)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
@@ -31,8 +31,6 @@ namespace CategoryTheory.Limits
 
 variable {C : Type u₁} [Category.{v₁} C]
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- Construct a cone for the empty diagram given an object. -/
 @[simps]
 def asEmptyCone (X : C) : Cone (Functor.empty.{0} C) :=

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Types.lean b/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@@ -48,8 +48,6 @@ open CategoryTheory Limits
 
 namespace CategoryTheory.Limits.Types
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`. -/
 @[simp 1001]
 theorem pi_lift_π_apply {β : Type u} (f : β → Type u) {P : Type u} (s : ∀ b, P ⟶ f b) (b : β)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean b/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
@@ -78,8 +78,6 @@ theorem zero_comp [HasZeroMorphisms C] {X : C} {Y Z : C} {f : Y ⟶ Z} :
   HasZeroMorphisms.zero_comp X f
 #align category_theory.limits.zero_comp CategoryTheory.Limits.zero_comp
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 instance hasZeroMorphismsPEmpty : HasZeroMorphisms (Discrete PEmpty) where
   Zero := by aesop_cat
 #align category_theory.limits.has_zero_morphisms_pempty CategoryTheory.Limits.hasZeroMorphismsPEmpty

diff --git a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
@@ -183,8 +183,6 @@ def BinaryFan.associatorOfLimitCone (L : ∀ X Y : C, LimitCone (pair X Y)) (X Y
     (L X (L Y Z).cone.pt).isLimit
 #align category_theory.limits.binary_fan.associator_of_limit_cone CategoryTheory.Limits.BinaryFan.associatorOfLimitCone
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- Construct a left unitor from specified limit cones.
 -/
 @[simps]

diff --git a/Mathlib/CategoryTheory/PEmpty.lean b/Mathlib/CategoryTheory/PEmpty.lean
@@ -16,8 +16,6 @@ import Mathlib.CategoryTheory.DiscreteCategory
 Defines a category structure on `PEmpty`, and the unique functor `PEmpty ⥤ C` for any category `C`.
 -/
 
--- Porting note: this file stressed Lean a good deal despite its length
-
 universe w v u
 -- morphism levels before object levels. See note [CategoryTheory universes].
 namespace CategoryTheory

diff --git a/Mathlib/CategoryTheory/StructuredArrow.lean b/Mathlib/CategoryTheory/StructuredArrow.lean
@@ -229,8 +229,6 @@ instance proj_reflectsIsomorphisms : ReflectsIsomorphisms (proj S T) where
 
 open CategoryTheory.Limits
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- The identity structured arrow is initial. -/
 def mkIdInitial [Full T] [Faithful T] : IsInitial (mk (𝟙 (T.obj Y))) where
   desc c := homMk (T.preimage c.pt.hom)
@@ -455,8 +453,6 @@ instance proj_reflectsIsomorphisms : ReflectsIsomorphisms (proj S T) where
 
 open CategoryTheory.Limits
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
-
 /-- The identity costructured arrow is terminal. -/
 def mkIdTerminal [Full S] [Faithful S] : IsTerminal (mk (𝟙 (S.obj Y))) where
   lift c := homMk (S.preimage c.pt.hom)