Near-timeout in `mulEnergy_card_filter`

Stream: mathlib4

[Anne Baanen]

#10765 trips over a timeout in Combinatorics.Additive.Energy, where docs#Finset.mulEnergy_eq_card_filter goes from 192815 heartbeats to 200322. Looks like the problem is the lemmas docs#Finset.filter_true_of_mem and docs#Finset.filter_false_of_mem which take 1.5s each to (fail to) discharge on each application, and they're applied at least twelve times (twice by each aesop and simp call).

[Anne Baanen]

I think it's a good idea to disable these simp lemmas either locally in that declaration or globally, what do you think?

[Anne Baanen]

For comparison, with attribute [-simp] Finset.filter_true_of_mem Finset.filter_false_of_mem the heartbeat count goes to 9060 (before #10765) or 10021 (after #10765).

[Yaël Dillies]

Oh thank you for investigating! This proof gave me a lot of trouble. With your change, can you make the proofs of the subgoal just a plain aesop without timing out?

[Anne Baanen]

Yes, the last line can become by aesop without timing out. It is quite a bit slower though, from near-instant to a few seconds on my machine.

[Yaël Dillies]

Then I'm glad my effort was not wasted. Do you want to open a PR to remove the simp tags?

[Anne Baanen]

(I did already! :D #12907)

[Matthew Ballard]

-400B instructions!?

[Johan Commelin]

@Matthew Ballard do you want to look into the non-linted simp more? Or shall we borsify this already?

[Matthew Ballard]

No. Let’s make the suggested change and go.

[Johan Commelin]

done

[Matthew Ballard]

Despite docs#Finset.filter_empty being solvable by simp, it needs to be fed as an argument downstream to a simp...

[Matthew Ballard]

Rebuilding locally with that now to see if there is only one such instance

[Matthew Ballard]

It was more economical to de-simp docs#Finset.filter_eq_self