no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap (fun x => (id x.fst, id x.snd)) (𝓤 α) = 𝓤 α
rw [← Prod.map_def, Prod.map_id, comap_id]