Sum.in[lr].inj in aesop

Stream: general

[Martin Dvořák]

How can I make aesop apply Sum.inl.inj and Sum.inr.inj to things it discovers itself?
I mean, the proof isn't a part of the context before calling aesop but after aesop runs, it has added a proof of Sum.inl x = Sum.inl y into the context. I want aesop to proceed to inferring x = y and close the goal with the knowledge.

[Michael Rothgang]

Does adding these lemmas to the aesop call do the trick? (Totally untested.)

[Martin Dvořák]

None of the "usual tricks" works for me.

[Martin Dvořák]

It needs to be done later than when aesop tends to apply these lemmas by default.

[František Silváši 🦉]

Maybe add safe forward Sum.inl_injective? (This might also need add simp Function.Injective combined.)

[Martin Dvořák]

It doesn't help. What I probably need is to run another simp phase at the end, or duplicate the rules to be not only in the simp phase but also in the other phase.

[Yury G. Kudryashov]

Do you have an #mwe?