case ha
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < index (↑{ carrier := K, isCompact' := h1K }) U

case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < index (↑K₀) U
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < prehaar (↑K₀) U { carrier := K, isCompact' := h1K }
apply div_pos <;> norm_cast
case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < index (↑K₀) U
case ha
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < index (↑{ carrier := K, isCompact' := h1K }) U

case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < index (↑K₀) U
apply index_pos ⟨⟨K, h1K⟩, h2K⟩ hU
no goals
case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
K : Set G
h1K : IsCompact K
h2K : Set.Nonempty (interior K)
⊢ 0 < index (↑K₀) U
exact index_pos K₀ hU