G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this :
  Classical.choose (_ : Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)) ∈
    ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
have := (Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this :
  ∀ (i : OpenNhdsOf 1),
    Classical.choose (_ : Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)) ∈ clPrehaar (↑K₀) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this :
  Classical.choose (_ : Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)) ∈
    ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
rw [mem_iInter] at this
no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf 1
this :
  ∀ (i : OpenNhdsOf 1),
    Classical.choose (_ : Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)) ∈ clPrehaar (↑K₀) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V
exact this V