no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.112580
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
c : α → β
h : ∀ (a b : α), c a = c b
this : (fun x => (c x.fst, c x.snd)) ⁻¹' idRel = univ
⊢ 𝓤 α ≤ comap (fun x => (c x.fst, c x.snd)) (𝓟 idRel)
simp [comap_principal, this, univ_mem]