-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem nonempty_iInter_clPrehaar (K₀ : PositiveCompacts G) :
    (haarProduct (K₀ : Set G) ∩ ⋂ V : OpenNhdsOf (1 : G), clPrehaar K₀ V).Nonempty

Proof state:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ ∀ (i : Compacts G), IsCompact (Icc 0 ↑(index ↑i ↑K₀))

Tactic:
intro K

Result:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ IsCompact (Icc 0 ↑(index ↑K ↑K₀))

Proof state:
case right.mk.a.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ V₀ ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen V₀ ∧ 1 ∈ V₀

Tactic:
exact ⟨Subset.trans (iInter_subset _ ⟨V, hV⟩) (iInter_subset _ h2V), h1V₀, h2V₀⟩

Result:
no goals

Proof state:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ ⋂ i ∈ t, clPrehaar (↑K₀) i

Tactic:
simp only [mem_iInter]

Result:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ ∀ i ∈ t, prehaar (↑K₀) V₀ ∈ clPrehaar (↑K₀) i

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
⊢ (haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty

Tactic:
let V₀ := ⋂ V ∈ t, (V : OpenNhdsOf (1 : G)).carrier

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
⊢ (haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ (haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty

Tactic:
refine ⟨prehaar K₀ V₀, ?_⟩

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i

Proof state:
case right.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ prehaar (↑K₀) V₀ ∈ clPrehaar ↑K₀ { toOpens := V, mem' := hV }

Tactic:
apply subset_closure

Result:
case right.mk.a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ prehaar (↑K₀) V₀ ∈ prehaar ↑K₀ '' {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}

Proof state:
case right.mk.a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ prehaar (↑K₀) V₀ ∈ prehaar ↑K₀ '' {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}

Tactic:
apply mem_image_of_mem

Result:
case right.mk.a.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ V₀ ∈ {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ (haarProduct ↑K₀ ∩ ⋂ V, clPrehaar (↑K₀) V).Nonempty

Tactic:
have : IsCompact (haarProduct (K₀ : Set G)) := by
  apply isCompact_univ_pi; intro K; apply isCompact_Icc

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
⊢ (haarProduct ↑K₀ ∩ ⋂ V, clPrehaar (↑K₀) V).Nonempty

Proof state:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ ∀ i ∈ t, prehaar (↑K₀) V₀ ∈ clPrehaar (↑K₀) i

Tactic:
rintro ⟨V, hV⟩ h2V

Result:
case right.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ prehaar (↑K₀) V₀ ∈ clPrehaar ↑K₀ { toOpens := V, mem' := hV }

Proof state:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ IsCompact (Icc 0 ↑(index ↑K ↑K₀))

Tactic:
apply isCompact_Icc

Result:
no goals

Proof state:
case mk.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
V : Set G
hV₁ : IsOpen V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
a✝ : { carrier := V, is_open' := hV₁, mem' := hV₂ } ∈ t
⊢ IsOpen { carrier := V, is_open' := hV₁, mem' := hV₂ }.carrier

Tactic:
exact hV₁

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
⊢ (haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty

Tactic:
have h2V₀ : (1 : G) ∈ V₀ := by simp only [V₀, mem_iInter]; rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₂

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ (haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty

Proof state:
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ (interior V₀).Nonempty

Tactic:
use 1

Result:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ 1 ∈ interior V₀