universe level が問題になる例: Prod

Prod を自作しようとしたところ、universe level 関連のエラーが出た。

inductive MyProd (α β : Type) : Type 1 where
  | mk (fst : α) (snd : β)

infix:20 " ×ₘ " => MyProd

#eval
  /-
  application type mismatch
    Nat ×ₘ (Int ×ₘ String)
  argument
    Int ×ₘ String
  has type
    Type 1 : Type 2
  but is expected to have type
    Type : Type 1
  -/
  let x : Nat ×ₘ (Int ×ₘ String) := ⟨1, ⟨2, "hello"⟩⟩

  let y : Nat ×ₘ (Int ×ₘ String) := ⟨1, 2, "hello"⟩
  x = y

Start by reproducing the self-contained Lean example in the issue and inspect the reported universe-level mismatch for the nested MyProd type. Determine whether the example should be corrected or documented, then verify that the intended product construction no longer produces the reported error.