Lean.Internal.coeM

Stream: lean4

[Marcus Rossel]

In the following (not quite minimal) example the goal of the last theorem is:

Lean.Internal.coeM (cmp? cmp rtr i) = cmp? cmp (Coe.coe rtr) i

The "Lean.Internal.coeM" sounds like something I shouldn't be seeing. Is this a bug, or is it fine here?

---

inductive Component
  | rtr

class ReactorType (α : Type _) where
  nest : α → Nat → Option α

namespace ReactorType

abbrev componentType [ReactorType α] : Component → Type _
  | .rtr => α

abbrev cmp? [inst : ReactorType α] : (cmp : Component) → α → Nat → Option (inst.componentType cmp)
  | .rtr => nest

instance [a : ReactorType α] [b : ReactorType β] [c : Coe α β] {cmp : Component} :
    Coe (a.componentType cmp) (b.componentType cmp) where
  coe :=
    match cmp with
    | .rtr => c.coe

theorem LawfulCoe.lower_cmp?
    [a : ReactorType α] [b : ReactorType β] [c : Coe α β] {rtr : α} {cmp} :
    (a.cmp? cmp rtr i : Option $ b.componentType cmp) = b.cmp? cmp rtr i := by