∀ {𝕜 : Type u_1} (h : RCLike 𝕜) (hk : NormedField 𝕜) (h'' : hk = h.toNormedField) (z : 𝕜),
  ‖z‖ ^ 2 =
    (⋯ ▸
            let __spread.0 := h.toNormedField;
            RCLike.re)
          z *
        (⋯ ▸
            let __spread.0 := h.toNormedField;
            RCLike.re)
          z +
      (⋯ ▸
            let __spread.0 := h.toNormedField;
            RCLike.im)
          z *
        (⋯ ▸
            let __spread.0 := h.toNormedField;
            RCLike.im)
          z