-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem le_index_mul (K₀ : PositiveCompacts G) (K : Compacts G) {V : Set G}
    (hV : (interior V).Nonempty) :
    index (K : Set G) V ≤ index (K : Set G) K₀ * index (K₀ : Set G) V

Proof state:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V

Tactic:
obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V

Proof state:
case intro.intro.intro.intro.hm.h.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = 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 ∈ t * s, (fun h => g * h) ⁻¹' V

Tactic:
exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ t.card * s.card

Tactic:
refine le_trans ?_ Finset.card_mul_le

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ (t * s).card

Proof state:
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V

Tactic:
have := h1t hg₂

Result:
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
this : g₁ * g₂ ∈ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V

Proof state:
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀ ⊆ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V

Tactic:
apply iUnion₂_subset

Result:
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ ∀ i ∈ s, (fun h => i * h) ⁻¹' ↑K₀ ⊆ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V

Tactic:
obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty

Result:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ (t * s).card

Tactic:
apply Nat.sInf_le

Result:
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ (t * s).card ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Proof state:
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ (t * s).card ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
refine ⟨_, ?_, rfl⟩

Result:
case intro.intro.intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ t * s ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Proof state:
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ ∀ (a : G), g₁ * a ∈ ↑K₀ → a ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V

Tactic:
intro g₂ hg₂

Result:
case intro.intro.intro.intro.hm.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V