simp! does not unfold abbrevs

Stream: mathlib4

[Yakov Pechersky]

In lean3, this works:

variables {α : Type*} [has_mul α] [inhabited α]

abbreviation Left (a : α) : α := a * default
abbreviation Right (a : α) : α := default * a

theorem mul_comm (a b : α) : a * b = b * a := sorry

example (a : α) : Left a = Right a := by simp! [mul_comm]

In mathlib4, one has to be more explicit:

variable {α : Type _} [Mul α] [Inhabited α]

abbrev Left (a : α) : α := a * default
abbrev Right (a : α): α := default * a

theorem mul_comm (a b : α) : a * b = b * a := sorry

example (a : α) : Left a = Right a := by
  simp! [mul_comm] -- doesn't solve
  sorry

example (a : α) : Left a = Right a := by
  simp! [Left, Right, mul_comm] -- even this doesn't solve
  sorry

example (a : α) : Left a = Right a := by simp [Left, Right, mul_comm] -- this does solve

[Mario Carneiro]

reported as lean4#1815