What type annotation can do

Stream: lean4

[Heather Macbeth]

In the mathlib4 port, I encountered a situation where type annotation was clearly doing something in Lean 3, but no longer does something in Lean 4. It was a term proof looking like

example (a b c : Units α) (h : a ≤ b) : c * a ≤ c * b :=
(mul_le_mul_left (h : (a : α) ≤ b) _ : (c : α) * a ≤ c * b)

and it works in Lean 3 but fails in Lean 4. Here is a full example (import-free but probably not minimal):
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/elaboration.20failure.20in.20algebra.2Eorder.2Egroup.2Eunits

[Kevin Buzzard]

The id trick works if you need a quick workaround:

example (a b c : Units α) (h : a ≤ b) : c * a ≤ c * b :=
mul_le_mul_left (id h : (a : α) ≤ b) _

[Heather Macbeth]

Oh sure, in fact the PR's already merged. Just wanted to flag the issue.