case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ index (↑K) V ≤ Finset.card t * Finset.card s
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
rw [← h2s, ← h2t, mul_comm]
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ index (↑K) V ≤ Finset.card (t * s)
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ index (↑K) V ≤ Finset.card t * Finset.card s
refine' le_trans _ Finset.card_mul_le
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ Finset.card (t * s) ∈ Finset.card '' {t | ↑K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ index (↑K) V ≤ Finset.card (t * s)
apply Nat.sInf_le
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ t * s ∈ {t | ↑K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ Finset.card (t * s) ∈ Finset.card '' {t | ↑K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
refine' ⟨_, _, rfl⟩
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ ↑K ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ t * s ∈ {t | ↑K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
rw [mem_setOf_eq]
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ (⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀) ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ ↑K ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
refine' Subset.trans h1s _
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ ∀ (i : G), i ∈ s → (fun h => i * h) ⁻¹' ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ (⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀) ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
apply iUnion₂_subset
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ (fun h => g₁ * h) ⁻¹' ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
⊢ ∀ (i : G), i ∈ s → (fun h => i * h) ⁻¹' ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
intro g₁ hg₁
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ ∀ (a : G), g₁ * a ∈ ↑K₀ → a ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ (fun h => g₁ * h) ⁻¹' ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
rw [preimage_subset_iff]
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ ∀ (a : G), g₁ * a ∈ ↑K₀ → a ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
intro g₂ hg₂
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
this : g₁ * g₂ ∈ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
have := h1t hg₂
case intro.intro.intro.intro.hm.h.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₁ * g₂ ∈ (fun h => (fun h => g₃ * h) ⁻¹' V) hg₃
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
this : g₁ * g₂ ∈ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩
case intro.intro.intro.intro.hm.h.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * g₁ * g₂ ∈ V
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.hm.h.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₁ * g₂ ∈ (fun h => (fun h => g₃ * h) ⁻¹' V) hg₃
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
rw [mem_preimage, ← mul_assoc] at h2V
no goals
case intro.intro.intro.intro.hm.h.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
s : Finset G
h1s : ↑K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' ↑K₀
h2s : Finset.card s = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * g₁ * g₂ ∈ V
⊢ g₂ ∈ ⋃ (g : G) (_ : g ∈ t * s), (fun h => g * h) ⁻¹' V
exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V