invalid `simp` theorem

Stream: mathlib4

[Markus Himmel]

I just looked at the file CategoryTheory/ConcreteCategory/Bundled.lean and was surprised that the following MWE now fails:

universe u v

namespace CategoryTheory

variable {c d : Type u → Type v} {α : Type u}

/-- `bundled` is a type bundled with a type class instance for that type. Only
the type class is exposed as a parameter. -/
-- @[nolint has_nonempty_instance]
structure Bundled (c : Type u → Type v) : Type max (u + 1) v where
  α : Type u
  str : c α := by infer_instance

instance : CoeSort (Bundled c) (Type u) :=
  ⟨Bundled.α⟩

@[simp]
theorem coe_mk (α) (str) : (@Bundled.mk c α str : Type u) = α :=
  rfl

end CategoryTheory

The error is invalid simp theorem, equation is equivalent to α = α. Indeed, by dsimp also proves the theorem. I believe mathlib3 has quite a few of these coe_mk lemmas. Are they just not needed anymore?

[Gabriel Ebner]

Yes, Lean 4 eagerly expands the coe notation. The ↑ etc. functions are no longer present in the elaborated term.

[Gabriel Ebner]

So the coe_mk is no longer needed because simp reduces (Bundled.mk α str).α to α by itself.