no goals
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
t : Finset G
ht : K ⊆ ⋃ (x : G) (h : x ∈ t), interior ((fun x_1 x_2 => x_1 * x_2) x ⁻¹' V)
⊢ ∃ t, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ (i : G), (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) i
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
⊢ K ⊆ ⋃ (i : G), (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) i
cases' hV with g₀ hg₀
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) (g₀ * g⁻¹)
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ (i : G), (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) i
refine' fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, _⟩
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => g₀ * g⁻¹ * id x) ⁻¹' interior V
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) (g₀ * g⁻¹)
refine' preimage_interior_subset_interior_preimage (continuous_const.mul continuous_id) _
no goals
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => g₀ * g⁻¹ * id x) ⁻¹' interior V
rwa [mem_preimage, id_def, inv_mul_cancel_right]