no goals
α✝ : Type ?u.661
β : Type ?u.664
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : Group α
h₁ : UniformContinuous fun p => p.fst * p.snd
h₂ : UniformContinuous fun p => p⁻¹
⊢ UniformContinuous fun p => p.fst / p.snd
simpa only [div_eq_mul_inv] using
h₁.comp (uniformContinuous_fst.prod_mk (h₂.comp uniformContinuous_snd))