simps with aliases

Stream: mathlib4

[Violeta Hernández]

In the CGT repo I've defined surreal cuts as a particular case of docs#Concept, so as to get the complete lattice instance for free. However, the extent and intent terminology makes no sense in this context (pun unintended), so I've defined a type alias, as well as aliases left = extent and right = intent. Is there any way I could configure the simps tactic so as to respect them?

Here's a toy example:

import Mathlib.Tactic.Simps.Basic

structure Foo where
  bar : Nat

abbrev Foo' := Foo
def Foo'.baz := Foo.bar

-- How do I tell `simps` to call the lemma `myFoo'_baz` instead?
@[simps!]
def myFoo' : Foo' := ⟨0⟩

[Edward van de Meent]

I seem to recall a command called something like initialize_simps_projection, which by name alone I'm guessing might do what you want?

[Edward van de Meent]

I have never used it though, so I could very well be wrong

[Edward van de Meent]

Still, I suspect that the attribute will have trouble not looking through the abbrev

[Violeta Hernández]

If it's needed I could just use a def rather than an abbrev, and declare the complete lattice instance I want manually.

[Violeta Hernández]

I'm also aware of initialize_simps_projection, and I'm also completely unaware of what it does.

[Christian Merten]

initialize_simps_projections Foo (bar → baz)