-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem index_pos (K : PositiveCompacts G) {V : Set G} (hV : (interior V).Nonempty) :
    0 < index (K : Set G) V

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ ∃ n, n ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
exact index_defined K.isCompact hV

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
⊢ False

Tactic:
obtain ⟨g, hg⟩ := K.interior_nonempty

Result:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ False

Proof state:
case h.e'_4
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ ⋃ g ∈ ∅, (fun h => g * h) ⁻¹' V = ∅

Tactic:
simp only [Finset.not_mem_empty, iUnion_of_empty, iUnion_empty]

Result:
no goals

Proof state:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ False

Tactic:
show g ∈ (∅ : Set G)

Result:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ g ∈ ∅

Proof state:
case h.e'_4
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ ∅ = ⋃ g ∈ ∅, (fun h => g * h) ⁻¹' V

Tactic:
symm

Result:
case h.e'_4
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ ⋃ g ∈ ∅, (fun h => g * h) ⁻¹' V = ∅

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

Tactic:
rw [Finset.card_eq_zero] at h2t

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

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

Tactic:
subst h2t

Result:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
⊢ False

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ ¬∃ x ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = 0

Tactic:
rintro ⟨t, h1t, h2t⟩

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

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

Tactic:
rw [index, Nat.sInf_def, Nat.find_pos, mem_image]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ ¬∃ x ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = 0

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ ∃ n, n ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Proof state:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ g ∈ ∅

Tactic:
convert h1t (interior_subset hg)

Result:
case h.e'_4
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ ∅ = ⋃ g ∈ ∅, (fun h => g * h) ⁻¹' V