∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] {g : β → γ} {f : α → β},
  UniformContinuous g →
    UniformContinuous f →
      UniformSpace.Completion.map g ∘ UniformSpace.Completion.map f = UniformSpace.Completion.map (g ∘ f)