∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : Monoid M] [inst_2 : MulAction M X]
  [inst_3 : UniformContinuousConstSMul M X],
  UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul M X =
    { toSMul := UniformSpace.Completion.instSMul M X, mul_smul := ⋯, one_smul := ⋯ }