case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
s : Finset G
h1s : K' ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K' V
⊢ index K V ≤ index K' V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
⊢ index K V ≤ index K' V
rcases index_elim hK' hV with ⟨s, h1s, h2s⟩
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
s : Finset G
h1s : K' ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K' V
⊢ index K' V ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
s : Finset G
h1s : K' ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K' V
⊢ index K V ≤ index K' V
apply Nat.sInf_le
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
s : Finset G
h1s : K' ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K' V
⊢ ∃ x, x ∈ {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∧ Finset.card x = index K' V
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
s : Finset G
h1s : K' ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K' V
⊢ index K' V ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
rw [mem_image]
no goals
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : Set.Nonempty (interior V)
s : Finset G
h1s : K' ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K' V
⊢ ∃ x, x ∈ {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∧ Finset.card x = index K' V
refine' ⟨s, Subset.trans h h1s, h2s⟩