∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] {β : Type u_2} [inst_2 : UniformSpace β] [inst_3 : Ring β]
  [IsTopologicalRing β] (f : α →+* β) [CompleteSpace β],
  Continuous fun x => UniformSpace.Completion.extension (⇑f) x.1 + UniformSpace.Completion.extension (⇑f) x.2