grind tagging for `Monotone`

Stream: mathlib4

[Sébastien Gouëzel]

In #34194 (+17/-82), I use grind to golf very tedious proofs on bounded variation functions (which I remember I struggled a lot to write in the first place). This is absolutely awesome, I invite you to have a look at the diff for a big smile.

Given that I use grind [Monotone] several times, I tried to tag Monotone with @[grind] (with different options) to make sure everyone would benefit from it. However, this breaks proofs (in this file and in other files) -- to see it, just start from the PR, add attribute [grind] Monotone just before the theorem add_point and see how it breaks the proof, at the line grind [Finset.sum_congr]. I tried several variants, writing and tagging custom lemmas, but to no avail. Is there no good way to tag Monotone for grind?

[Robin Carlier]

I’ve had the same experience as well when experimenting.
Given that grind has special support for orders via its order module, is it reasonable to expect Core to eventually add a monotone module to grind?
cc @Kim Morrison

[Jakub Nowak]

The fun_prop tactic doesn't work for Monotone goals?

[Michael Rothgang]

So far, Monotone (and its basic lemmas) have not been tagged with fun_prop --- so it doesn't. Feel free to make a PR changing this.