case a
α : Type u
β : Type u_1
γ : Type ?u.419491
δ : Type ?u.419494
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ uniformity α = uniformity α
α : Type u
β : Type u_1
γ : Type ?u.419491
δ : Type ?u.419494
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ UniformSpace.comap (↑h) inst✝² = inst✝³
ext : 1
no goals
case a
α : Type u
β : Type u_1
γ : Type ?u.419491
δ : Type ?u.419494
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ uniformity α = uniformity α
exact h.uniformInducing.comap_uniformity