MyProp.congr_* lemmas, LHS vs RHS

Stream: mathlib4

[Yury G. Kudryashov]

When we have (h : MyProp a b), then some congr lemmas assume that ha and hb in (h.congr ha hb : MyProp a' b') have the form a = a', b = b', while other lemmas expect a' = a, b' = b (and similary for other assumptions like docs#Filter.EventuallyEq, docs#Set.EqOn). E.g., we have docs#ContinuousAt.congr and docs#ContinuousAt.congr_of_eventuallyEq that differ by EventuallyEq.symm. Which convention should we use?

[Eric Wieser]

I would expect a signature of the form a = a' -> P a -> P a'

[Yury G. Kudryashov]

Also, once we make a decision (so far, a = a' wins, but it's been only 25 minutes), should I go and change lemmas in place, or create new ones & leave the old ones as deprecated?

[Yury G. Kudryashov]

@Eric Wieser Do you think the order of a = a' and P a is important?

[Eric Wieser]

I don't think it's as important as being consistent about the = direction, but I do prefer that order

[Yury G. Kudryashov]

Currently, most of topology&analysis congr lemmas (both asymptotics and continuity/differentiability) put P a first.

[Jireh Loreaux]

I think this order: P.congr : P a → a = a' → P a' is common for the following reason. Often you know P a and you then supply a (sometimes long) proof of a = a'. So, if hPa : P a you can write apply P.congr hPa and then your goal will be a = a', whereas in the reverse argument order, you would have to write apply P.congr ?_ hPa. Of course, if you use dot notation, this is moot because apply hPa.congr will generally work.

[Jireh Loreaux]

Of course, this is a very minor point, but I think it might explain the slight preference for that order.

[Yury G. Kudryashov]

I have an idea why so many lemmas in topology/analysis use a' = a. We want to show that some function is nice at a point. We simplify it near this point (so, we have f = f' with a simpler f'). Then we have MyProp f' and f = f', so this order avoids .symm here and there.

[Yury G. Kudryashov]

I'm going to wait for a day or two before going forward with swapping LHS and RHS in these lemmas.

[Yury G. Kudryashov]

@Sébastien Gouëzel WDYT? It looks like you've added some (most?) of the congr_of_eventuallyEq lemmas.

[Sébastien Gouëzel]

I think coherence throughout the library is important. So changing the lemmas so that they all use the same order looks definitely like a good idea to me!

[Patrick Massot]

Even nicer would be to have some kind of linter enforcing consistency.

[Sébastien Gouëzel]

And documenting this in one of our documentation files.

[Yury G. Kudryashov]

To minimize merge conflicts, I would prefer to get #34965 merged first, then I can open a PR swapping LHS with RHS in all these congr lemmas.