case intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
t : Finset G
ht : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
rcases compact_covered_by_mul_left_translates hK hV with ⟨t, ht⟩
no goals
case intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
t : Finset G
ht : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
exact ⟨t.card, t, ht, rfl⟩