Attribute to map rewrite rules through a functor?

Stream: Is there code for X?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The category theory library has a useful attribute, @[reassoc], to generate a lemma f ≫ (g ≫ a) = h ≫ a from f ≫ g = h; simp can apply the former but not the latter after reassociating to the right. Another thing that sometimes happens is that we want to apply F.map f ≫ F.map g = F.map h as a simp rule, but this also will not trigger from just the original lemma; is there an attribute to automatically generate this (perhaps quantifying over all F)?

[Adam Topaz]

i think grind is supposed to eesolve all such issues

[Adam Topaz]

but the answer is no.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Is there a writeup anywhere of how grind will deal with situations like this one? In the meantime, I wrote the attribute by copy-pasting reassoc.

[Yaël Dillies]

Just to flag that @Andrew Yang have the same thought as you in the context of Toric

[Andrew Yang]

I suggest we have this in mathlib and tag every category theory lemma with this.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It would be quite a lot of lemmas added to the simp set.. I am mostly using these in a particular situation where we work with yoneda.map a lot. You also run into the funny situation of needing all of f ≫ g = h, f ≫ (g ≫ a) = h ≫ a, F.map f ≫ F.map g = F.map h, and F.map f ≫ (F.map g ≫ a) = F.map h ≫ a which is achieved via the monstrous @[functor_map (attr := reassoc (attr := simp))].

[Kevin Buzzard]

you might call it monstrous but it's pretty cool if that works.

[Yaël Dillies]

I think that actually the lemmas that are eligible for this new kind of auxiliary lemma generation are the same that are available for reassoc. So I think we don't need a new attribute at all, but merely an extension of reassoc.

[Robin Carlier]

If you want to make it an extension of reassoc, be aware that I have an open PR (#24303) modifying reassoc, so there might be some conflicts in the code.