aesop forward reasoning; regression in Mathlib

Stream: general

[Kim Morrison]

@Jannis Limperg, just FYI, I added

#adaptation_note
/--
The `by measurability` argument of `lintegral_iSup` became slower after
https://github.com/leanprover-community/aesop/pull/199 was merged,
resulting in this declaration now requiring a larger `maxHeartbeats` limit.
-/
set_option maxHeartbeats 400000 in

in #22334.

[Jannis Limperg]

Thanks for the ping! I have an idea what might be causing this and will look at it tomorrow.

[Jannis Limperg]

fix: #22394

[Eric Wieser]

Duplicating lemmas with Not unfolded doesn't seem ideal; should aesop have special support for unfolding Not?

[Jannis Limperg]

Yes it should. :) I just need to decide to what degree this should be automatic.

[Jannis Limperg]

aesop#197