Custom simp for simplifying integrals

Stream: mathlib4

[David Ledvinka]

When working with lintegrals you frequently have to use rw when you would really like to use simp because of Measurable or MeasurableSet side conditions. I recently noticed that if you set the discharger to measurability or fun_prop it can be useable. However there are many lemmas which are not simp lemmas (likely because of these side conditions) which would be desirable with this discharger. Would it be best to just tag them as simp anyway or use a custom tactic with a custom simp set? Or perhaps someone has other ideas entirely.

Note I would also like this to work for the Bochner integral eventually as well, but there is currently no automation for integrability (I think fun_prop could be made to handle some easy but useful cases).

[Jovan Gerbscheid]

Might solving lean#3475 fix your problems as well?

[David Ledvinka]

Thanks for pointing that out to me! If I understand the proposal correctly I don't think that exactly helps unless we add autoparams for every measurability goal, but perhaps that could be done (manually or automatically).

[Jovan Gerbscheid]

Indeed, we'd still have to add the autoParams to the relevant simp lemmas. But it does mean that the simp lemmas will work out of the box, without needing to specify the custom discharger.