α : Type ?u.118853
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : Group β
ι : Sort u_1
us' : ι → UniformSpace β
h' : ∀ (i : ι), UniformGroup β
⊢ UniformGroup β
α : Type ?u.118853
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : Group β
ι : Sort u_1
us' : ι → UniformSpace β
h' : ∀ (i : ι), UniformGroup β
⊢ UniformGroup β
rw [← sInf_range]
no goals
α : Type ?u.118853
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : Group β
ι : Sort u_1
us' : ι → UniformSpace β
h' : ∀ (i : ι), UniformGroup β
⊢ UniformGroup β
exact uniformGroup_sInf (Set.forall_range_iff.mpr h')