Computability/AkraBazzi

Stream: mathlib4

[Kim Morrison]

@Frédéric Dupuis (or anyone else interested) could you please look at the proof of T_isBigO_smoothingFn_mul_asympBound in Computability.AkraBazzi. This is now timing out on nightly-testing, but I'm inclined to believe it is the proof's fault for being too long, not Lean's fault.

A refactor on master would be much appreciated! :-)

[Frédéric Dupuis]

I just had a look, and it seems like the culprit was a slow aesop call. Should I just make a regular PR and leave it at that?

[Kim Morrison]

Yes, please!

[Frédéric Dupuis]

#12541