∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformContinuousConstSMul 𝕜 E], ⇑UniformSpace.Completion.toComplL = UniformSpace.Completion.coe'