simps generates useless lemmas

Stream: mathlib4

[Adam Topaz]

In the porting PR !4#2767 specifically here you will notice a pretty silly simps! declaration.

The reason for this is that simps! alone generated some useless lemmas that the simpNF linter caught. These lemmas were of the form _ = _ where both _ are proofs of some proposition. The lean3 version of one such lemma is here:
docs#category_theory.limits.cone.equiv_costructured_arrow_functor_map_right_down_down

Is there a way to tell simps in lean4 to not generate a particular lemma (or lemmas) while generating all others?
Is there a way to tell simps in lean4 to not generate worthless lemmas which prove that two proofs are equal?

[Adam Topaz]

ping @Floris van Doorn

[Floris van Doorn]

You can use @[simps (config := { notRecursive := [`PLift, `Ulift] })] to not apply projections of certain structures (you probably only need one of them, presumably ULift).
Currently simps indeed doesn't check whether the lemmas it generates are propositional, in the rare case that a projection is sometimes propositional and sometimes data.
Generating all default lemmas except some that you list is currently not supported, but on the wishlist.

[Adam Topaz]

Thanks! The nonrecursive option should work well in this case.