no goals
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β✝
inst✝² : UniformSpace γ
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ↑f
h₂ : UniformContinuous ↑f.symm
⊢ comap (Prod.map ↑f ↑f) (𝓤 β) ≤ 𝓤 α
rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]