∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α],
  UniformSpace.Completion.mapRingHom (RingHom.id α) ⋯ = RingHom.id (UniformSpace.Completion α)