feat(tactic/simps): some improvements (#5541)

* `@[simps]` would previously fail if the definition is not a constructor application (with the suggestion to add option `{rhs_md := semireducible}` and maybe `simp_rhs := tt`). Now it automatically adds `{rhs_md := semireducible, simp_rhs := tt}` whenever it reaches this situation. 
* Remove all (now) unnecessary occurrences of `{rhs_md := semireducible}` from the library. There are still a couple left where the `simp_rhs := tt` is undesirable.
* `@[simps {simp_rhs := tt}]` now also applies `dsimp, simp` to the right-hand side of the lemmas it generates.
* Add some `@[simps]` in `category_theory/limits/cones.lean`
* `@[simps]` would not recursively apply projections of `prod` or `pprod`. This is now customizable with the `not_recursive` option.
* Add an option `trace.simps.debug` with some debugging information.

Author: fpvandoorn

src/algebra/category/Algebra/limits.lean

@@ -88,10 +88,10 @@ begin
   refine is_limit.of_faithful
     (forget (Algebra R)) (types.limit_cone_is_limit _)
     (λ s, { .. }) (λ s, rfl),
-  { simp only [forget_map_eq_coe, alg_hom.map_one, functor.map_cone_π], refl, },
-  { intros x y, simp only [forget_map_eq_coe, alg_hom.map_mul, functor.map_cone_π], refl, },
-  { simp only [forget_map_eq_coe, alg_hom.map_zero, functor.map_cone_π], refl, },
-  { intros x y, simp only [forget_map_eq_coe, alg_hom.map_add, functor.map_cone_π], refl, },
+  { simp only [forget_map_eq_coe, alg_hom.map_one, functor.map_cone_π_app], refl, },
+  { intros x y, simp only [forget_map_eq_coe, alg_hom.map_mul, functor.map_cone_π_app], refl, },
+  { simp only [forget_map_eq_coe, alg_hom.map_zero, functor.map_cone_π_app], refl, },
+  { intros x y, simp only [forget_map_eq_coe, alg_hom.map_add, functor.map_cone_π_app], refl, },
   { intros r, ext j, exact (s.π.app j).commutes r,  },
 end
 

src/algebra/category/Group/basic.lean

@@ -198,13 +198,13 @@ namespace category_theory.iso
 
 /-- Build a `mul_equiv` from an isomorphism in the category `Group`. -/
 @[to_additive AddGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category
-`AddGroup`.", simps {rhs_md := semireducible}]
+`AddGroup`.", simps]
 def Group_iso_to_mul_equiv {X Y : Group} (i : X ≅ Y) : X ≃* Y :=
 i.hom.to_mul_equiv i.inv i.hom_inv_id i.inv_hom_id
 
 /-- Build a `mul_equiv` from an isomorphism in the category `CommGroup`. -/
 @[to_additive AddCommGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism
-in the category `AddCommGroup`.", simps {rhs_md := semireducible}]
+in the category `AddCommGroup`.", simps]
 def CommGroup_iso_to_mul_equiv {X Y : CommGroup} (i : X ≅ Y) : X ≃* Y :=
 i.hom.to_mul_equiv i.inv i.hom_inv_id i.inv_hom_id
 

src/algebra/category/Group/limits.lean

@@ -264,7 +264,7 @@ end
 The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
 agrees with the `subtype` map.
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def kernel_iso_ker_over {G H : AddCommGroup.{u}} (f : G ⟶ H) :
   over.mk (kernel.ι f) ≅ @over.mk _ _ G (AddCommGroup.of f.ker) (add_subgroup.subtype f.ker) :=
 over.iso_mk (kernel_iso_ker f) (by simp)

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -252,7 +252,7 @@ def colimit_cocone_is_colimit (F : J ⥤ PresheafedSpace C) : is_colimit (colimi
     have t : m.base = colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).map_cocone s),
     { ext,
       dsimp,
-      simp only [colimit.ι_desc_apply, map_cocone_ι],
+      simp only [colimit.ι_desc_apply, map_cocone_ι_app],
       rw ← w j,
       simp, },
     fapply PresheafedSpace.ext, -- could `ext` please not reorder goals?

src/category_theory/Fintype.lean

@@ -40,7 +40,7 @@ instance {X : Fintype} : fintype X := X.2
 instance : category Fintype := induced_category.category bundled.α
 
 /-- The fully faithful embedding of `Fintype` into the category of types. -/
-@[derive [full, faithful], simps {rhs_md:=semireducible}]
+@[derive [full, faithful], simps]
 def incl : Fintype ⥤ Type* := induced_functor _
 
 instance : concrete_category Fintype := ⟨incl⟩

src/category_theory/adjunction/basic.lean

@@ -351,7 +351,7 @@ def left_adjoint_of_equiv : C ⥤ D :=
 
 /-- Show that the functor given by `left_adjoint_of_equiv` is indeed left adjoint to `G`. Dual
 to `adjunction_of_equiv_right`. -/
-@[simps {rhs_md := semireducible}]
+@[simps]
 def adjunction_of_equiv_left : left_adjoint_of_equiv e he ⊣ G :=
 mk_of_hom_equiv
 { hom_equiv := e,
@@ -390,7 +390,7 @@ def right_adjoint_of_equiv : D ⥤ C :=
 
 /-- Show that the functor given by `right_adjoint_of_equiv` is indeed right adjoint to `F`. Dual
 to `adjunction_of_equiv_left`. -/
-@[simps {rhs_md := semireducible}]
+@[simps]
 def adjunction_of_equiv_right : F ⊣ right_adjoint_of_equiv e he :=
 mk_of_hom_equiv
 { hom_equiv := e,
@@ -419,7 +419,7 @@ def to_equivalence (adj : F ⊣ G) [∀ X, is_iso (adj.unit.app X)] [∀ Y, is_i
 If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise)
 isomorphisms, then the functor is an equivalence of categories.
 -/
-@[simps {rhs_md := semireducible}]
+@[simps]
 def is_right_adjoint_to_is_equivalence [is_right_adjoint G]
   [∀ X, is_iso ((adjunction.of_right_adjoint G).unit.app X)]
   [∀ Y, is_iso ((adjunction.of_right_adjoint G).counit.app Y)] :

src/category_theory/currying.lean

@@ -89,7 +89,7 @@ def curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E)) :=
 /--
 The equivalence of functor categories given by currying/uncurrying.
 -/
-@[simps {rhs_md := semireducible}] -- create projection simp lemmas even though this isn't a `{ .. }`.
+@[simps] -- create projection simp lemmas even though this isn't a `{ .. }`.
 def currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E) :=
 equivalence.mk uncurry curry
   (nat_iso.of_components (λ F, nat_iso.of_components

src/category_theory/equivalence.lean

@@ -272,7 +272,7 @@ by { dsimp [inv_fun_id_assoc], tidy }
 by { dsimp [inv_fun_id_assoc], tidy }
 
 /-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
-@[simps functor inverse unit_iso counit_iso {rhs_md:=semireducible}]
+@[simps functor inverse unit_iso counit_iso]
 def congr_left (e : C ≌ D) : (C ⥤ E) ≌ (D ⥤ E) :=
 equivalence.mk
   ((whiskering_left _ _ _).obj e.inverse)
@@ -281,7 +281,7 @@ equivalence.mk
   (nat_iso.of_components (λ F, e.inv_fun_id_assoc F) (by tidy))
 
 /-- If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`. -/
-@[simps functor inverse unit_iso counit_iso {rhs_md:=semireducible}]
+@[simps functor inverse unit_iso counit_iso]
 def congr_right (e : C ≌ D) : (E ⥤ C) ≌ (E ⥤ D) :=
 equivalence.mk
   ((whiskering_right _ _ _).obj e.functor)

src/category_theory/essential_image.lean

@@ -68,7 +68,7 @@ lemma obj_mem_ess_image (F : D ⥤ C) (Y : D) : F.obj Y ∈ ess_image F := ⟨Y,
 instance : category F.ess_image := category_theory.full_subcategory _
 
 /-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
-@[derive [full, faithful], simps {rhs_md := semireducible}]
+@[derive [full, faithful], simps]
 def ess_image_inclusion (F : C ⥤ D) : F.ess_image ⥤ D :=
 full_subcategory_inclusion _
 
@@ -85,7 +85,7 @@ def to_ess_image (F : C ⥤ D) : C ⥤ F.ess_image :=
 The functor `F` factorises through its essential image, where the first functor is essentially
 surjective and the second is fully faithful.
 -/
-@[simps {rhs_md := semireducible}]
+@[simps]
 def to_ess_image_comp_essential_image_inclusion :
   F.to_ess_image ⋙ F.ess_image_inclusion ≅ F :=
 nat_iso.of_components (λ X, iso.refl _) (by tidy)

src/category_theory/limits/cones.lean

@@ -30,25 +30,17 @@ variables {J C} (F : J ⥤ C)
 natural transformations from the constant functor with value `X` to `F`.
 An object representing this functor is a limit of `F`.
 -/
+@[simps]
 def cones : Cᵒᵖ ⥤ Type v := (const J).op ⋙ (yoneda.obj F)
 
-lemma cones_obj (X : Cᵒᵖ) : F.cones.obj X = ((const J).obj (unop X) ⟶ F) := rfl
-
-@[simp] lemma cones_map_app {X₁ X₂ : Cᵒᵖ} (f : X₁ ⟶ X₂) (t : F.cones.obj X₁) (j : J) :
-  (F.cones.map f t).app j = f.unop ≫ t.app j := rfl
-
 /--
 `F.cocones` is the functor assigning to an object `X` the type of
 natural transformations from `F` to the constant functor with value `X`.
 An object corepresenting this functor is a colimit of `F`.
 -/
+@[simps]
 def cocones : C ⥤ Type v := const J ⋙ coyoneda.obj (op F)
 
-lemma cocones_obj (X : C) : F.cocones.obj X = (F ⟶ (const J).obj X) := rfl
-
-@[simp] lemma cocones_map_app {X₁ X₂ : C} (f : X₁ ⟶ X₂) (t : F.cocones.obj X₁) (j : J) :
-  (F.cocones.map f t).app j = t.app j ≫ f := rfl
-
 end functor
 
 section
@@ -167,7 +159,7 @@ def equiv (F : J ⥤ C) : cocone F ≅ Σ X, F.cocones.obj X :=
 { X := X,
   ι := c.extensions.app X f }
 
-@[simp] lemma extend_ι  (c : cocone F) {X : C} (f : c.X ⟶ X) :
+@[simp] lemma extend_ι (c : cocone F) {X : C} (f : c.X ⟶ X) :
   (extend c f).ι = c.extensions.app X f :=
 rfl
 
@@ -280,17 +272,11 @@ def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
 The categories of cones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
 (possibly after changing the indexing category by an equivalence).
 -/
+@[simps functor_obj]
 def equivalence_of_reindexing {K : Type v} [small_category K] {G : K ⥤ C}
   (e : K ≌ J) (α : e.functor ⋙ F ≅ G) : cone F ≌ cone G :=
 (whiskering_equivalence e).trans (postcompose_equivalence α)
 
-@[simp]
-lemma equivalence_of_reindexing_functor_obj {K : Type v} [small_category K] {G : K ⥤ C}
-  (e : K ≌ J) (α : e.functor ⋙ F ≅ G) (c : cone F) :
-  (equivalence_of_reindexing e α).functor.obj c =
-  (postcompose α.hom).obj (cone.whisker e.functor c) :=
-rfl
-
 section
 variable (F)
 
@@ -447,17 +433,11 @@ def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) :
 The categories of cocones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
 (possibly after changing the indexing category by an equivalence).
 -/
+@[simps functor_obj]
 def equivalence_of_reindexing {K : Type v} [small_category K] {G : K ⥤ C}
   (e : K ≌ J) (α : e.functor ⋙ F ≅ G) : cocone F ≌ cocone G :=
 (whiskering_equivalence e).trans (precompose_equivalence α.symm)
 
-@[simp]
-lemma equivalence_of_reindexing_functor_obj {K : Type v} [small_category K] {G : K ⥤ C}
-  (e : K ≌ J) (α : e.functor ⋙ F ≅ G) (c : cocone F) :
-  (equivalence_of_reindexing e α).functor.obj c =
-  (precompose α.inv).obj (cocone.whisker e.functor c) :=
-rfl
-
 section
 variable (F)
 
@@ -535,25 +515,19 @@ variables {F : J ⥤ C} {G : J ⥤ C} (H : C ⥤ D)
 open category_theory.limits
 
 /-- The image of a cone in C under a functor G : C ⥤ D is a cone in D. -/
+@[simps]
 def map_cone   (c : cone F)   : cone (F ⋙ H)   := (cones.functoriality F H).obj c
 /-- The image of a cocone in C under a functor G : C ⥤ D is a cocone in D. -/
+@[simps]
 def map_cocone (c : cocone F) : cocone (F ⋙ H) := (cocones.functoriality F H).obj c
 
-@[simp] lemma map_cone_X (c : cone F) : (H.map_cone c).X = H.obj c.X := rfl
-@[simp] lemma map_cocone_X (c : cocone F) : (H.map_cocone c).X = H.obj c.X := rfl
-
 /-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially.  -/
 def map_cone_morphism   {c c' : cone F}   (f : c ⟶ c')   :
   H.map_cone c ⟶ H.map_cone c' := (cones.functoriality F H).map f
 /-- Given a cocone morphism `c ⟶ c'`, construct a cocone morphism on the mapped cocones functorially.  -/
 def map_cocone_morphism {c c' : cocone F} (f : c ⟶ c') :
   H.map_cocone c ⟶ H.map_cocone c' := (cocones.functoriality F H).map f
 
-@[simp] lemma map_cone_π (c : cone F) (j : J) :
-  (map_cone H c).π.app j = H.map (c.π.app j) := rfl
-@[simp] lemma map_cocone_ι (c : cocone F) (j : J) :
-  (map_cocone H c).ι.app j = H.map (c.ι.app j) := rfl
-
 /-- If `H` is an equivalence, we invert `H.map_cone` and get a cone for `F` from a cone
 for `F ⋙ H`.-/
 def map_cone_inv [is_equivalence H]
@@ -587,7 +561,7 @@ def map_cocone_inv_map_cocone {F : J ⥤ D} (H : D ⥤ C) [is_equivalence H] (c
 (limits.cocones.functoriality_equivalence F (as_equivalence H)).unit_iso.symm.app c
 
 /-- `functoriality F _ ⋙ postcompose (whisker_left F _)` simplifies to `functoriality F _`. -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def functoriality_comp_postcompose {H H' : C ⥤ D} (α : H ≅ H') :
   cones.functoriality F H ⋙ cones.postcompose (whisker_left F α.hom) ≅ cones.functoriality F H' :=
 nat_iso.of_components (λ c, cones.ext (α.app _) (by tidy)) (by tidy)
@@ -597,7 +571,7 @@ For `F : J ⥤ C`, given a cone `c : cone F`, and a natural isomorphism `α : H
 `H H' : C ⥤ D`, the postcomposition of the cone `H.map_cone` using the isomorphism `α` is
 isomorphic to the cone `H'.map_cone`.
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def postcompose_whisker_left_map_cone {H H' : C ⥤ D} (α : H ≅ H') (c : cone F) :
   (cones.postcompose (whisker_left F α.hom : _)).obj (H.map_cone c) ≅ H'.map_cone c :=
 (functoriality_comp_postcompose α).app c
@@ -607,7 +581,7 @@ def postcompose_whisker_left_map_cone {H H' : C ⥤ D} (α : H ≅ H') (c : cone
 natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious ways of producing
 a cone over `G ⋙ H`, and they are both isomorphic.
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def map_cone_postcompose {α : F ⟶ G} {c} :
   H.map_cone ((cones.postcompose α).obj c) ≅
   (cones.postcompose (whisker_right α H : _)).obj (H.map_cone c) :=
@@ -616,14 +590,14 @@ cones.ext (iso.refl _) (by tidy)
 /--
 `map_cone` commutes with `postcompose_equivalence`
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def map_cone_postcompose_equivalence_functor {α : F ≅ G} {c} :
   H.map_cone ((cones.postcompose_equivalence α).functor.obj c) ≅
     (cones.postcompose_equivalence (iso_whisker_right α H : _)).functor.obj (H.map_cone c) :=
 cones.ext (iso.refl _) (by tidy)
 
 /-- `functoriality F _ ⋙ precompose (whisker_left F _)` simplifies to `functoriality F _`. -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def functoriality_comp_precompose {H H' : C ⥤ D} (α : H ≅ H') :
    cocones.functoriality F H ⋙ cocones.precompose (whisker_left F α.inv)
  ≅ cocones.functoriality F H' :=
@@ -634,7 +608,7 @@ For `F : J ⥤ C`, given a cocone `c : cocone F`, and a natural isomorphism `α
 `H H' : C ⥤ D`, the precomposition of the cocone `H.map_cocone` using the isomorphism `α` is
 isomorphic to the cocone `H'.map_cocone`.
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def precompose_whisker_left_map_cocone {H H' : C ⥤ D} (α : H ≅ H') (c : cocone F) :
   (cocones.precompose (whisker_left F α.inv : _)).obj (H.map_cocone c) ≅ H'.map_cocone c :=
 (functoriality_comp_precompose α).app c
@@ -644,7 +618,7 @@ def precompose_whisker_left_map_cocone {H H' : C ⥤ D} (α : H ≅ H') (c : coc
 `c : cocone F`, a natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious
 ways of producing a cocone over `G ⋙ H`, and they are both isomorphic.
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def map_cocone_precompose {α : F ⟶ G} {c} :
   H.map_cocone ((cocones.precompose α).obj c) ≅
   (cocones.precompose (whisker_right α H : _)).obj (H.map_cocone c) :=
@@ -653,7 +627,7 @@ cocones.ext (iso.refl _) (by tidy)
 /--
 `map_cocone` commutes with `precompose_equivalence`
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def map_cocone_precompose_equivalence_functor {α : F ≅ G} {c} :
   H.map_cocone ((cocones.precompose_equivalence α).functor.obj c) ≅
     (cocones.precompose_equivalence (iso_whisker_right α H : _)).functor.obj (H.map_cocone c) :=
@@ -664,15 +638,15 @@ variables {K : Type v} [small_category K]
 /--
 `map_cone` commutes with `whisker`
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def map_cone_whisker {E : K ⥤ J} {c : cone F} :
   H.map_cone (c.whisker E) ≅ (H.map_cone c).whisker E :=
 cones.ext (iso.refl _) (by tidy)
 
 /--
 `map_cocone` commutes with `whisker`
 -/
-@[simps {rhs_md:=semireducible}]
+@[simps]
 def map_cocone_whisker {E : K ⥤ J} {c : cocone F} :
   H.map_cocone (c.whisker E) ≅ (H.map_cocone c).whisker E :=
 cocones.ext (iso.refl _) (by tidy)
@@ -762,25 +736,23 @@ variables {F : J ⥤ Cᵒᵖ}
 /-- Change a cocone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
 -- Here and below we only automatically generate the `@[simp]` lemma for the `X` field,
 -- as we can write a simpler `rfl` lemma for the components of the natural transformation by hand.
-@[simps X] def cone_of_cocone_left_op (c : cocone F.left_op) : cone F :=
+@[simps {rhs_md := semireducible, simp_rhs := tt}]
+def cone_of_cocone_left_op (c : cocone F.left_op) : cone F :=
 { X := op c.X,
   π := nat_trans.remove_left_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) }
 
-@[simp] lemma cone_of_cocone_left_op_π_app (c : cocone F.left_op) (j) :
-  (cone_of_cocone_left_op c).π.app j = (c.ι.app (op j)).op :=
-by { dsimp [cone_of_cocone_left_op], simp }
-
 /-- Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.left_op : Jᵒᵖ ⥤ C`. -/
-@[simps X] def cocone_left_op_of_cone (c : cone F) : cocone (F.left_op) :=
+@[simps {rhs_md := semireducible, simp_rhs := tt}]
+def cocone_left_op_of_cone (c : cone F) : cocone (F.left_op) :=
 { X := unop c.X,
   ι := nat_trans.left_op c.π }
 
-@[simp] lemma cocone_left_op_of_cone_ι_app (c : cone F) (j) :
-  (cocone_left_op_of_cone c).ι.app j = (c.π.app (unop j)).unop :=
-by { dsimp [cocone_left_op_of_cone], simp }
-
 /-- Change a cone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
-@[simps X] def cocone_of_cone_left_op (c : cone F.left_op) : cocone F :=
+/- When trying use `@[simps]` to generate the `ι_app` field of this definition, `@[simps]` tries to
+  reduce the RHS using `expr.dsimp` and `expr.simp`, but for some reason the expression is not
+  being simplified properly. -/
+@[simps X]
+def cocone_of_cone_left_op (c : cone F.left_op) : cocone F :=
 { X := op c.X,
   ι := nat_trans.remove_left_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) }
 
@@ -789,14 +761,11 @@ by { dsimp [cocone_left_op_of_cone], simp }
 by { dsimp [cocone_of_cone_left_op], simp }
 
 /-- Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.left_op : Jᵒᵖ ⥤ C`. -/
-@[simps X] def cone_left_op_of_cocone (c : cocone F) : cone (F.left_op) :=
+@[simps {rhs_md := semireducible, simp_rhs := tt}]
+def cone_left_op_of_cocone (c : cocone F) : cone (F.left_op) :=
 { X := unop c.X,
   π := nat_trans.left_op c.ι }
 
-@[simp] lemma cone_left_op_of_cocone_π_app (c : cocone F) (j) :
-  (cone_left_op_of_cocone c).π.app j = (c.ι.app (unop j)).unop :=
-by { dsimp [cone_left_op_of_cocone], simp }
-
 end
 
 end category_theory.limits