{M : Type u_1} →
  [inst : TopologicalSpace M] →
    [inst_1 : Mul M] →
      {motive : ContinuousMul M → Sort u} →
        (t : ContinuousMul M) → ((continuous_mul : Continuous fun p => p.1 * p.2) → motive ⋯) → motive t