Automation & opposite categories

Stream: mathlib4

[Brendan Seamas Murphy]

In the definition of the monoidal category instance on the opposite category we have to explicitly write out Quiver.Hom.unop_inj <| by simp to prove the laws instead of the proofs being generated by aesop_cat. The obstruction to aesop_cat being able to prove these is that CategoryTheory.op_comp rewrites in the wrong direction (for this). We can get around this by making Quiver.Hom.unop_inj a local @[ext] lemma, but for a similar problem in the other direction ("unop"ing an op-ed structure and deriving the laws for it) this solution doesn't work, since Quiver.Hom.op_inj is always valid to apply. Is there any clever trick with aesop we could here? It seems like CategoryTheory.op_comp is directed correctly, but otoh it seems like in a lot of cases we're going to want to automatically generate proofs which use it to rewrite the other way

[Kevin Buzzard]

I don't really know the first thing about tactics but I'll comment that your situation reminds me a bit of the problem we had with trying to do casts using simp, when sometimes we wanted to pull the coercions out and other times push them in as far as possible, so there was no good choice for simp lemma direction. This was ultimately fixed by not using simp and writing entirely new tactics norm_cast and push_cast.

[Brendan Seamas Murphy]

Hm, that does seem like a similar problem!

[Adam Topaz]

All metaprogramming contributions are greatly appreciated :)