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