feat: erw?, a tool to explain why erw is necessary #21643

Stream: PR reviews

[Kim Morrison]

I delayed writing this for far too long, but it turns out to have been quite straightforward to get something minimal working. I haven't tested much yet, but I invite others to do so too! :-)

From the PR description: in

def subalgebraMap (e : A ≃ₐ[R] B) (S : Subalgebra R A) : S ≃ₐ[R] S.map (e : A →ₐ[R] B) :=
  { e.toRingEquiv.subsemiringMap S.toSubsemiring with
    commutes' := fun r => by
      ext; dsimp only
      erw [RingEquiv.subsemiringMap_apply_coe]
      exact e.commutes _ }

replace erw with erw?. You'll get the informational message:

(e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun
  and
⇑(e.toRingEquiv.subsemiringMap S.toSubsemiring)
  are defeq at default transparency, but not at reducible transparency.

[Kim Morrison]

(The implementation doesn't hook into the implementation of erw at all --- it simply inspects the term that it produces. Realising that this was enough explains why the implementation is much easier than I'd expected/feared.)

[Damiano Testa]

#21643

[Kim Morrison]

@Damiano Testa, I used some tricks to abbreviate your message collection code: state transformers and a macro! :-)

[Damiano Testa]

Great, I like it!

[Eric Wieser]

Do we want to use the widget diff view here, to deal with highlighting the mismatching subexpressions?

[Kim Morrison]

Happy to have that added/replaced, but can we proceed with merging this one first? I want to go hunt erws.

[Damiano Testa]

I am happy to merge as is and fix/upgrade in production.

[Damiano Testa]

Btw, I think that erw? can be "silent" and hence might survive into final code: should erw? either always emit a message or be linted?

[Kim Morrison]

Oh, that's a good point.

[Kim Morrison]

Sorry, I need to sleep now. Please feel free to take if off the queue, or we can make this modification later, as you think best.

[Damiano Testa]

Simply adding a log saying "Testing erw" will make CI catch it.

[Damiano Testa]

I see that Eric is making suggestions: I will remove it from the queue, apply the suggestions and then merge again.

[Damiano Testa]

The erw? tactic has been merged! It has not been tested very much, so, if you use it and notice some roughness, feel free to report any issues!