simps

Stream: mathlib4

[Scott Morrison]

@Floris van Doorn, just calling your attention to a query about simps at !4#3193.

When doing definitions of morphisms in the opposite category (i.e. when constructing functors), the simps tag would create lemmas _unop (like _hom_app_unop if we define a natural transformation). I had to occasionally require only simps lemmas like hom_app, inv_app, etc, instead of hom_app_unop, inv_app_unop). I do not know if it is possible to make this automatic by using a suitable initalize_simps_projection command [doing initalize_simps_projection Opposite (-unop) would just create no simp lemma at all].

Is there a way to achieve this?

[Floris van Doorn]

(@Joël Riou) For a single simp attribute you can use @[simps (config := { notRecursive := [`Opposite] })]. You can do this globally by adding `Opposite to this line:
https://github.com/leanprover-community/mathlib4/blob/f5de05f35eda950d292d655dd165f9412207ce34/Mathlib/Tactic/Simps/Basic.lean#L837

[Scott Morrison]

Thanks, I've incorporated this into the PR.