congr_arg not unifying HMul

Stream: mathlib4

[Yakov Pechersky]

Consider:

variable [Mul α]

example (a b c : α) : a = c → a * b = c * b :=
  congrArg _ -- doesn't work

example (a b c : α) : a = c → a * b = c * b :=
  congrArg (· * b) -- does work, because resolves the HMul problem

example (a b c : α) : a = c → b * a = b * c :=
  congrArg _ -- left-multiplication works

Does one now always need to assist in unification of right-multiplication?

[Mario Carneiro]

I wouldn't really expect that to work. Does it work in lean 3?

[Mario Carneiro]

my recollection is that you almost always have to give the function like in your second example (the third example is a fairly rare case)