no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
⊢ 0 < ↑(index (↑K₀.toCompacts) U)
exact_mod_cast index_pos K₀ hU