exact? -> congr()?

Stream: lean4

[Julian Berman]

Is it feasible / has it been considered to have exact? suggest uses of congr() rather than congrArg / congrFun etc.? Looking at have foo := congr($this * (foo bar)) is so much easier on the eyes than exact? suggesting have foo := congrFun (congrArg HMul.hMul this) (foo bar)

[Kim Morrison]

I think step 1 would be to write a delaborator that expresses congrFun and congrArg in terms of congr. If that could be made to work, even if it is not turned on by default, one could probably engineer exact? to make use of it.