case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ index ((fun h => g * h) '' K) V ≤ index K V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
⊢ index ((fun h => g * h) '' K) V ≤ index K V
rcases index_elim hK hV with ⟨s, h1s, h2s⟩
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ index ((fun h => g * h) '' K) V ≤ Finset.card s
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ index ((fun h => g * h) '' K) V ≤ index K V
rw [← h2s]
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ Finset.card s ∈ Finset.card '' {t | (fun h => g * h) '' 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 : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ index ((fun h => g * h) '' K) V ≤ Finset.card s
apply Nat.sInf_le
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ ∃ x, x ∈ {t | (fun h => g * h) '' K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∧ Finset.card x = Finset.card s
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ Finset.card s ∈ Finset.card '' {t | (fun h => g * h) '' K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
rw [mem_image]
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s ∈
    {t | (fun h => g * h) '' K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ ∃ x, x ∈ {t | (fun h => g * h) '' K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∧ Finset.card x = Finset.card s
refine' ⟨s.map (Equiv.mulRight g⁻¹).toEmbedding, _, Finset.card_map _⟩
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ (fun h => g * h) '' K ⊆
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s ∈
    {t | (fun h => g * h) '' K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
simp only [mem_setOf_eq]
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ ((fun h => g * h) '' ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) ⊆
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ (fun h => g * h) '' K ⊆
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
refine' Subset.trans (image_subset _ h1s) _
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₁ ∈ (fun h => (fun h => g₂ * h) ⁻¹' V) hg₂
⊢ (fun h => g * h) g₁ ∈
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
⊢ ((fun h => g * h) '' ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) ⊆
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
rintro _ ⟨g₁, ⟨_, ⟨g₂, rfl⟩, ⟨_, ⟨hg₂, rfl⟩, hg₁⟩⟩, rfl⟩
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ (fun h => g * h) g₁ ∈
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₁ ∈ (fun h => (fun h => g₂ * h) ⁻¹' V) hg₂
⊢ (fun h => g * h) g₁ ∈
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
simp only [mem_preimage] at hg₁
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ ∃ a, a ∈ s ∧ a * g⁻¹ * (g * g₁) ∈ V
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ (fun h => g * h) g₁ ∈
    ⋃ (g_1 : G) (_ : g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s), (fun h => g_1 * h) ⁻¹' V
simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight,
  exists_exists_and_eq_and, mem_preimage, Equiv.toEmbedding_apply]
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ g₂ * g⁻¹ * (g * g₁) ∈ V
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ ∃ a, a ∈ s ∧ a * g⁻¹ * (g * g₁) ∈ V
refine' ⟨_, hg₂, _⟩
no goals
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : Set.Nonempty (interior V)
g : G
s : Finset G
h1s : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ g₂ * g⁻¹ * (g * g₁) ∈ V
simp only [mul_assoc, hg₁, inv_mul_cancel_left]