G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ index K V ≤ index ((fun h => g * h) '' K) V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ index ((fun h => g * h) '' K) V = index K V
refine' le_antisymm (mul_left_index_le hK hV g) _
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ K = (fun h => g⁻¹ * h) '' ((fun b => g * b) '' K)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ index K V ≤ index ((fun h => g * h) '' K) V
convert mul_left_index_le (hK.image <| continuous_mul_left g) hV g⁻¹
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ K = (fun x => g⁻¹ * (g * x)) '' K
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ K = (fun h => g⁻¹ * h) '' ((fun b => g * b) '' K)
rw [image_image]
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ (fun x => g⁻¹ * (g * x)) '' K = K
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ K = (fun x => g⁻¹ * (g * x)) '' K
symm
case h.e'_2.h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
h : G
⊢ g⁻¹ * (g * h) = h
case h.e'_3.h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
⊢ (fun x => g⁻¹ * (g * x)) '' K = K
convert image_id' _ with h
no goals
case h.e'_2.h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : Set.Nonempty (interior V)
h : G
⊢ g⁻¹ * (g * h) = h
apply inv_mul_cancel_left