{M : Type u_2} →
  {α : Type u_3} →
    [inst : SMul M α] →
      [inst_1 : MeasurableSpace M] →
        [inst_2 : MeasurableSpace α] →
          {motive : MeasurableSMul₂ M α → Sort u} →
            ((measurable_smul : Measurable (Function.uncurry fun x1 x2 => x1 • x2)) → motive ⋯) →
              (t : MeasurableSMul₂ M α) → motive t