G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)
have : IsCompact (haarProduct (K₀ : Set G)) := by
  apply isCompact_univ_pi; intro K; apply isCompact_Icc
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (V : OpenNhdsOf 1), clPrehaar (↑K₀) V)
refine' this.inter_iInter_nonempty (clPrehaar K₀) (fun s => isClosed_closure) fun t => _
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
let V₀ := ⋂ V ∈ t, (V : OpenNhdsOf (1 : G)).carrier
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
have h1V₀ : IsOpen V₀ := by
  apply isOpen_biInter; apply Finset.finite_toSet; rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₁
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
have h2V₀ : (1 : G) ∈ V₀ := by simp only [mem_iInter]; rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₂
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ Set.Nonempty (haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i)
refine' ⟨prehaar K₀ V₀, _⟩
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ haarProduct ↑K₀

case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ haarProduct ↑K₀ ∩ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i
constructor
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
⊢ ∀ (i : Compacts G), IsCompact (Icc 0 ↑(index ↑i ↑K₀))
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
⊢ IsCompact (haarProduct ↑K₀)
apply isCompact_univ_pi
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ IsCompact (Icc 0 ↑(index ↑K ↑K₀))
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
⊢ ∀ (i : Compacts G), IsCompact (Icc 0 ↑(index ↑i ↑K₀))
intro K
no goals
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ IsCompact (Icc 0 ↑(index ↑K ↑K₀))
apply isCompact_Icc
case hs
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ Set.Finite fun i => i ∈ t.val

case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ ∀ (i : OpenNhdsOf 1), (i ∈ fun i => i ∈ t.val) → IsOpen i.carrier
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ IsOpen V₀
apply isOpen_biInter
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ ∀ (i : OpenNhdsOf 1), (i ∈ fun i => i ∈ t.val) → IsOpen i.carrier
case hs
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ Set.Finite fun i => i ∈ t.val

case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ ∀ (i : OpenNhdsOf 1), (i ∈ fun i => i ∈ t.val) → IsOpen i.carrier
apply Finset.finite_toSet
case h.mk.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
V : Set G
hV₁ : IsOpen V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
a✝ : { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ } ∈ fun i => i ∈ t.val
⊢ IsOpen { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ }.toOpens.carrier
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
⊢ ∀ (i : OpenNhdsOf 1), (i ∈ fun i => i ∈ t.val) → IsOpen i.carrier
rintro ⟨⟨V, hV₁⟩, hV₂⟩ _
no goals
case h.mk.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
V : Set G
hV₁ : IsOpen V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
a✝ : { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ } ∈ fun i => i ∈ t.val
⊢ IsOpen { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ }.toOpens.carrier
exact hV₁
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
⊢ ∀ (i : OpenNhdsOf 1), i ∈ t → 1 ∈ i.carrier
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
⊢ 1 ∈ V₀
simp only [mem_iInter]
case mk.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
V : Set G
hV₁ : IsOpen V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
i✝ : { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ } ∈ t
⊢ 1 ∈ { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ }.toOpens.carrier
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
⊢ ∀ (i : OpenNhdsOf 1), i ∈ t → 1 ∈ i.carrier
rintro ⟨⟨V, hV₁⟩, hV₂⟩ _
no goals
case mk.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
V : Set G
hV₁ : IsOpen V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
i✝ : { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ } ∈ t
⊢ 1 ∈ { toOpens := { carrier := V, is_open' := hV₁ }, mem' := hV₂ }.toOpens.carrier
exact hV₂
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ Set.Nonempty (interior V₀)
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ haarProduct ↑K₀
apply prehaar_mem_haarProduct K₀
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ 1 ∈ interior V₀
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ Set.Nonempty (interior V₀)
use 1
no goals
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ 1 ∈ interior V₀
rwa [h1V₀.interior_eq]
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ ∀ (i : OpenNhdsOf 1), i ∈ t → prehaar (↑K₀) (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈ clPrehaar (↑K₀) i
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ ⋂ (i : OpenNhdsOf 1) (_ : i ∈ t), clPrehaar (↑K₀) i
simp only [mem_iInter]
case right.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : 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 : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈ clPrehaar ↑K₀ { toOpens := V, mem' := hV }
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
⊢ ∀ (i : OpenNhdsOf 1), i ∈ t → prehaar (↑K₀) (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈ clPrehaar (↑K₀) i
rintro ⟨V, hV⟩ h2V
case right.mk.a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : 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 : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈
    prehaar ↑K₀ '' {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}
case right.mk
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : 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 : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈ clPrehaar ↑K₀ { toOpens := V, mem' := hV }
apply subset_closure
case right.mk.a.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈ {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}
case right.mk.a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : 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 : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈
    prehaar ↑K₀ '' {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}
apply mem_image_of_mem
case right.mk.a.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧
    IsOpen (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∧ 1 ∈ ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
case right.mk.a.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∈ {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen U ∧ 1 ∈ U}
rw [mem_setOf_eq]
no goals
case right.mk.a.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
h1V₀ : IsOpen V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧
    IsOpen (⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier) ∧ 1 ∈ ⋂ (V : OpenNhdsOf 1) (_ : V ∈ t), V.carrier
exact ⟨Subset.trans (iInter_subset _ ⟨V, hV⟩) (iInter_subset _ h2V), h1V₀, h2V₀⟩