congrArg or congr_arg

Stream: mathlib4

[Kevin Buzzard]

Searching in mathlib4 gives me 86 congrArgs (mostly in dependencies but some in Mathlib) and 100 congr_args (all in Mathlib). Have we been doing it wrong in Mathlib?

[Mario Carneiro]

congr_arg itself is defined in mathlib

[Mario Carneiro]

the one in core is called congrArg

[Mario Carneiro]

When congrArg was written the naming convention was far from settled (in fact it dates back to the time when all lean 4 theorems were in camel case)

[Mario Carneiro]

I think at this point it is safe to say that it should be called congr_arg