no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ Quotient.mk (separationSetoid γ) ∘ g ∘ f = (map g ∘ map f) ∘ Quotient.mk (separationSetoid α)
simp only [Function.comp, map_mk, hf, hg]