Rewriting by an a.e. equality in an integral

Stream: general

[Aaron Hill]

When rewriting by an equality, I'll often use conv => equals <new_rhs> to obtain a goal of the form <lhs> = <new_rhs>. However, I need to rewrite an integral using an inequality that only holds almost everywhere (MeasureTheory.integral_congr_ae). Is there anything similar to the conv => equals pattern that would allow me to perform a targeted rewrite within an integral along an almost-everywhere equal relation, without needing to write out the full expression?

Currently, I'm relying on copy-pasting the entire expression from the infoview and fixing pretty-printing roundtrip issues

[Michael Rothgang]

Can grw do it/should it be able to?

[David Ledvinka]

Unfortunately grw cannot handle this currently, see #mathlib4 > Announcement: New `grw` tactic @ 💬
(there is some discussion in that thread about possibly updating rw and grw to handle bound variables in the future)

I have ran into this kind of thing a lot and found a few tricks to avoid rewriting the whole thing but unfortunately no catch all solution (which grw could possibly be if it could handle bound variables). Perhaps write a #mwe.

[Jovan Gerbscheid]

@Aaron Hill could you share a #mwe?

It is true that grw currently can't rewrite under binders, but in such a situation you can use the gcongr tactic, in combination with a calc block.