{α : Type u_3} →
  {β : Type u_4} →
    [inst : Norm α] →
      [inst_1 : Norm β] →
        [inst_2 : SMul α β] →
          {motive : NormSMulClass α β → Sort u} →
            (t : NormSMulClass α β) → ((norm_smul : ∀ (r : α) (x : β), ‖r • x‖ = ‖r‖ * ‖x‖) → motive ⋯) → motive t