case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : CompactSpace G
⊢ Continuous fun p => p.fst / p.snd
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : CompactSpace G
⊢ UniformContinuous fun p => p.fst / p.snd
apply CompactSpace.uniformContinuous_of_continuous
no goals
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : CompactSpace G
⊢ Continuous fun p => p.fst / p.snd
exact continuous_div'