simps and mem

Stream: general

[Bhavik Mehta]

Can I convince simps to generate lemmas with name mem_? For example, here: https://github.com/leanprover-community/mathlib/blob/d3897413bcab8250914ea34e97c369ea4e74b0cf/src/category_theory/sites/pretopology.lean#L154 the simps on the structure before that makes the right simp lemma but calls it to_grothendieck_mem instead of mem_to_grothendieck (like the manually generated one below). Is there a way to make simps always give the name mem_ when used on these structures?

[Bhavik Mehta]

(the simps projections are made here: https://github.com/leanprover-community/mathlib/blob/d3897413bcab8250914ea34e97c369ea4e74b0cf/src/category_theory/sites/grothendieck.lean#L86)

[Eric Wieser]

It would be cool if simps could take {}_apply as the custom name instead of just apply, then the use case above would be mem_{}

[Floris van Doorn]

There is currently no way to do this, but I could add that ability.

@Eric Wieser: do you expect any use cases other than adding a prefix or postfix?

[Floris van Doorn]

@Bhavik Mehta Does the def simps.sieves trick indeed let @[simps] generate the correct lemma (using ∈)?
That's pretty neat, I didn't realize that would work.

[Bhavik Mehta]

Yeah! I was a bit surprised by that too, the generated lemma is syntactically the same as the one I put below