no goals
α : Type u
β : Type u_1
γ : Type ?u.411266
δ : Type ?u.411269
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ UniformInducing (↑(UniformEquiv.symm h) ∘ ↑h)
simp only [symm_comp_self, uniformInducing_id]