no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t, t ∈ 𝓤 β ∧ ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) = 𝓤 α
simp [eq_comm, Filter.ext_iff, subset_def, h]