aesop change breaking Mathlib

Stream: mathlib4

[Scott Morrison]

@Jannis Limperg, I can't bump Mathlib to the latest aesop (see #7973), because of your commit https://github.com/leanprover-community/aesop/commit/6749fa4e776919514dae85bfc0ad62a511bc42a7.

We get errors of the form:

attribute [aesop (rule_sets [Measurable]) unfold norm] npowRec   -- Declaration 'npowRec' cannot be unfolded.

[Scott Morrison]

Ah, the discussion here is relevant.

[Scott Morrison]

I'm testing out just removing the rules that aesop now rejects. So far so good?

[Scott Morrison]

No, unfortunately there is then a continuity failure in Mathlib.Analysis.NormedSpace.HomeomorphBall.

[Scott Morrison]

Okay, in order to keep up with Std, I am no longer going to try bumping aesop in #7973.

[Jannis Limperg]

You could also bump Aesop to 5e016236e9e699691aaa9872fa380df12cd7f677 (one commit below current master).