Congruence for integrals

Stream: mathlib4

[Yuval Filmus]

In a recent proof, I used IntervalIntegral.integral_congr.
Is there any reason this isn't tagged @congr?
Same for IntervalIntegrable.congr and similar lemmas for other integrals.

One possible reason is that there are actually many congr lemmas, and it's unclear which one to use, but in that case we could make the "obvious" one (which plays nicely with the iterative nature of congr) the "default".

[Ruben Van de Velde]

Might well be "nobody tried it yet"

[Sébastien Gouëzel]

Often we're looking at set integrals, and then the right congr lemma wouldn't be the same one (it would be that the two functions coincide on the set, and moreover the set is measurable). There's also the fact that equality of integrals is true if the functions are equal almost everywhere, and often that's the version you want. So the "right" lemma to use really depends on the specifics of the situation.

[Jovan Gerbscheid]

The gcongr tactic/tag is also relevant here. In particular the version assuming almost everywhere equality is probably good to tag with gcongr.

When it comes to side conditions like only requiring the equality on a set, you can make a higher priority congr/gcongr lemma for this, so that it can fire instead of the more generic version.