RFC: Increase precedence of $ in congr()

Stream: mathlib4

[Yaël Dillies]

I often find myself wanting to turn an equality h : a = b into a new equality h' : a.foo = b.foo. congr() is an amazing tool for this, except that its syntax is quite disappointing when it comes to projections: One cannot simply write congr($h.foo) as it gets parsed as congr($(h.foo)) but instead one needs the slightly mouthful congr(($h).foo).

[Yaël Dillies]

There are very few times where one would quote a proof with dots in (in fact, it has yet to happen to me!). The cases I can think of are:

1. Lemmas with dot notation with a single argument and which returns an equality. The only such lemma I can find is docs#Eq.symm.
2. Declarations proving an equality in an unopened namespace. Empirically, it seems to be very rare to want to quote a global declaration, probably because congr() is a great way to prove easy corollaries, and easy corollaries of existing declarations in mathlib are usually already stated next to them.

[Yaël Dillies]

Therefore I would like to suggest swapping the precedence of $ and . in congr(). What do people think? Concretely, here's an example:

import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic.TermCongr

-- works, but so many brackets!
example {m n : ℕ} (h : m + 1 = n + 1) :
    (m + 1) * m.factorial = (n + 1) * n.factorial :=
  congr(($h).factorial)

-- doesn't work, but I would like it to
example {m n : ℕ} (h : m + 1 = n + 1) :
    (m + 1) * m.factorial = (n + 1) * n.factorial :=
  congr($h.factorial)
/-
Invalid field `factorial`: The environment does not contain `Eq.factorial`
  h
has type
  m + 1 = n + 1
-/

[Kenny Lau]

well, personal experience is not a good indicator, can you search /congr\(.+\$\w+\.\w+/ vs /congr\(.+\$\w+\)\.\w+/ on github?

[Eric Wieser]

I think it would be confusing to change the precedence in congr() without also doing other antiquotations like q() and `()

[Eric Wieser]

(which makes this a Lean RFC)