awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) / (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
congr_arg (fun x : ℝ => x / index K₀ U) ?_

Premises used: HDiv.hDiv, Nat.cast, MeasureTheory.Measure.haar.index, congr_arg, SetLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
refine :
  (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) / (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
refine congr_arg (fun x : ℝ => x / index K₀ U) ?_

Premises used: HDiv.hDiv, Nat.cast, MeasureTheory.Measure.haar.index, congr_arg, SetLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)

Tactic:
mod_cast index_union_eq K₁ K₂ hU h

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast, MeasureTheory.Measure.haar.index, SetLike.coe, Max.max, MeasureTheory.Measure.haar.index_union_eq, Nat.cast_inj._simp_1, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)

Tactic:
exact mod_cast index_union_eq K₁ K₂ hU h

Premises used: MeasureTheory.Measure.haar.index_union_eq
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
g : G
K : Compacts G
⊢ prehaar (↑K₀ : Set G) U (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = prehaar (↑K₀ : Set G) U K

Tactic:
simp only [prehaar, Compacts.coe_map, is_left_invariant_index K.isCompact _ hU]

Premises used: TopologicalSpace.Compacts.coe_map, MeasureTheory.Measure.haar.is_left_invariant_index, TopologicalSpace.Compacts.isCompact, MeasureTheory.Measure.haar.prehaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
h : Membership.mem (γ := Set (Compacts G)) univ { carrier := K, isCompact' := hK : Compacts G }
⊢ 0 ≤ prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := hK : Compacts G } ∧
    prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := hK : Compacts G } ≤
      (↑(index (↑{ carrier := K, isCompact' := hK : Compacts G } : Set G) (↑K₀ : Set G)) : ℝ)

Tactic:
⟨prehaar_nonneg K₀ _, prehaar_le_index K₀ _ hU⟩

Premises used: MeasureTheory.Measure.haar.prehaar_le_index, MeasureTheory.Measure.haar.prehaar_nonneg, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
h : Membership.mem (γ := Set (Compacts G)) univ { carrier := K, isCompact' := hK : Compacts G }
⊢ 0 ≤ prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := hK : Compacts G } ∧
    prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := hK : Compacts G } ≤
      (↑(index (↑{ carrier := K, isCompact' := hK : Compacts G } : Set G) (↑K₀ : Set G)) : ℝ)

Tactic:
exact ⟨prehaar_nonneg K₀ _, prehaar_le_index K₀ _ hU⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
h : ∀ (i : Compacts G), IsCompact (X := ℝ) (Icc 0 (↑(index (↑i : Set G) (↑K₀ : Set G)) : ℝ))
⊢ IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))

Tactic:
apply isCompact_univ_pi

Premises used: isCompact_univ_pi
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ IsCompact (X := ℝ) (Icc 0 (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ))

Tactic:
apply isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))

Tactic:
have : IsCompact (haarProduct (K₀ : Set G)) := by
    apply isCompact_univ_pi; intro K; apply isCompact_Icc
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
⊢ Set.Nonempty (α := Compacts G → ℝ)
    (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V)

Tactic:
this.inter_iInter_nonempty (clPrehaar K₀) (fun s => isClosed_closure) fun t => ?_

Premises used: MeasureTheory.Measure.haar.clPrehaar, IsCompact.inter_iInter_nonempty, SetLike.coe, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
refine :
  ∀ (t : Finset (OpenNhdsOf (α := G) 1)),
    Set.Nonempty (α := Compacts G → ℝ) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
⊢ Set.Nonempty (α := Compacts G → ℝ)
    (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V)

Tactic:
refine this.inter_iInter_nonempty (clPrehaar K₀) (fun s => isClosed_closure) fun t => ?_

Premises used: MeasureTheory.Measure.haar.clPrehaar, IsCompact.inter_iInter_nonempty, SetLike.coe, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
V : Set G
hV₁ : IsOpen[inst_1] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ : Opens G }.carrier
h : { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 } ∈ t
⊢ IsOpen[inst_1] { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 }.carrier

Tactic:
hV₁
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
V : Set G
hV₁ : IsOpen[inst_1] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ : Opens G }.carrier
h : { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 } ∈ t
⊢ IsOpen[inst_1] { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 }.carrier

Tactic:
exact hV₁
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
⊢ IsOpen[inst_1] V₀

Tactic:
have h1V₀ : IsOpen V₀ := isOpen_biInter_finset <| by rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₁
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
simp : ∀ (i : OpenNhdsOf (α := G) 1) (i_1 : i ∈ t), 1 ∈ i.carrier
⊢ 1 ∈ V₀

Tactic:
simp only [V₀, mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
V : Set G
hV₁ : IsOpen[inst_1] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ : Opens G }.carrier
i : { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 } ∈ t
⊢ 1 ∈ { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 }.carrier

Tactic:
hV₂

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
V : Set G
hV₁ : IsOpen[inst_1] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ : Opens G }.carrier
i : { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 } ∈ t
⊢ 1 ∈ { carrier := V, is_open' := hV₁, mem' := hV₂ : OpenNhdsOf (α := G) 1 }.carrier

Tactic:
exact hV₂
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
⊢ 1 ∈ V₀

Tactic:
have h2V₀ : (1 : G) ∈ V₀ := by simp only [V₀, mem_iInter]; rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₂
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
⊢ Set.Nonempty (α := Compacts G → ℝ) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)

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

Premises used: Set.Nonempty, SetLike.coe, Exists.intro, MeasureTheory.Measure.haar.prehaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
refine :
  Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
    (prehaar (↑K₀ : Set G) V₀)
⊢ Set.Nonempty (α := Compacts G → ℝ) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)

Tactic:
refine ⟨prehaar K₀ V₀, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
left : Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G)) (prehaar (↑K₀ : Set G) V₀)
right : Membership.mem (γ := Set (Compacts G → ℝ)) (⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i) (prehaar (↑K₀ : Set G) V₀)
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
    (prehaar (↑K₀ : Set G) V₀)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
left : (interior V₀).Nonempty
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G)) (prehaar (↑K₀ : Set G) V₀)

Tactic:
apply prehaar_mem_haarProduct K₀

Premises used: MeasureTheory.Measure.haar.prehaar_mem_haarProduct
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
h : 1 ∈ interior V₀
⊢ (interior V₀).Nonempty

Tactic:
use 1
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ h h₁ h₂ h₃ : 1 ∈ V₀
⊢ 1 ∈ interior V₀

Tactic:
rwa [h1V₀.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
right : ∀ (i : OpenNhdsOf (α := G) 1) (i_1 : i ∈ t), prehaar (↑K₀ : Set G) V₀ ∈ clPrehaar (↑K₀ : Set G) i
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i) (prehaar (↑K₀ : Set G) V₀)

Tactic:
simp only [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 } ∈ t
right :
  Membership.mem (γ := Set (Compacts G → ℝ))
    (prehaar (↑K₀ : Set G) ''
      {U : Set G |
        U ⊆ (↑{ toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U})
    (prehaar (↑K₀ : Set G) V₀)
⊢ prehaar (↑K₀ : Set G) V₀ ∈ clPrehaar (↑K₀ : Set G) { toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 } ∈ t
right :
  Membership.mem (γ := Set (Set G))
    {U : Set G | U ⊆ (↑{ toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}
    V₀
⊢ Membership.mem (γ := Set (Compacts G → ℝ))
    (prehaar (↑K₀ : Set G) ''
      {U : Set G |
        U ⊆ (↑{ toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U})
    (prehaar (↑K₀ : Set G) V₀)

Tactic:
apply mem_image_of_mem

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 } ∈ t
⊢ V₀ ⊆ (↑{ toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧ IsOpen[inst_1] V₀ ∧ 1 ∈ V₀

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

Premises used: Set.Subset.trans, And.intro, Set.iInter_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst_1] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 } ∈ t
⊢ V₀ ⊆ (↑{ toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧ IsOpen[inst_1] V₀ ∧ 1 ∈ V₀

Tactic:
exact ⟨Subset.trans (iInter_subset _ ⟨V, hV⟩) (iInter_subset _ h2V), h1V₀, h2V₀⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G)) (chaar K₀)

Tactic:
(Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).1

Premises used: MeasureTheory.Measure.haar.chaar, Set.Mem, Classical.choose_spec, And.left, MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf (α := G) 1
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V)
    (Classical.choose (p :=
      Membership.mem (γ := Set (Compacts G → ℝ))
        (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V))
      ⋯)

Tactic:
have := (Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).2
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf (α := G) 1
this :
  Membership.mem (γ := Set (Compacts G → ℝ)) (⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V)
    (Classical.choose (p :=
      Membership.mem (γ := Set (Compacts G → ℝ))
        (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V))
      ⋯)
⊢ ∀ (i : OpenNhdsOf (α := G) 1),
    Classical.choose (p :=
        Membership.mem (γ := Set (Compacts G → ℝ))
          (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V))
        ⋯ ∈
      clPrehaar (↑K₀ : Set G) i

Tactic:
rw [mem_iInter] at this

Premises used: Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf (α := G) 1
this :
  ∀ (i : OpenNhdsOf (α := G) 1),
    Classical.choose (p :=
        Membership.mem (γ := Set (Compacts G → ℝ))
          (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V))
        ⋯ ∈
      clPrehaar (↑K₀ : Set G) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀ : Set G) V

Tactic:
this V

Premises used: MeasureTheory.Measure.haar.chaar, Set.Mem
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
V : OpenNhdsOf (α := G) 1
this :
  ∀ (i : OpenNhdsOf (α := G) 1),
    Classical.choose (p :=
        Membership.mem (γ := Set (Compacts G → ℝ))
          (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V))
        ⋯ ∈
      clPrehaar (↑K₀ : Set G) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀ : Set G) V

Tactic:
exact this V
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ Membership.mem (γ := Set ((fun (a : Compacts G) ↦ ℝ) K))
    ((fun (K : Compacts G) ↦ (Icc 0 (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) : Set ℝ)) K) (chaar K₀ K)

Tactic:
have := chaar_mem_haarProduct K₀ K (mem_univ _)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this :
  Membership.mem (γ := Set ((fun (a : Compacts G) ↦ ℝ) K))
    ((fun (K : Compacts G) ↦ (Icc 0 (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) : Set ℝ)) K) (chaar K₀ K)
⊢ 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)

Tactic:
rw [mem_Icc] at this

Premises used: Set.mem_Icc
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)
⊢ 0 ≤ chaar K₀ K

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)
⊢ 0 ≤ chaar K₀ K

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
⊢ Continuous eval

Tactic:
have : Continuous eval := continuous_apply ⊥
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
this : Continuous eval
change : chaar K₀ ∈ eval ⁻¹' {0}
⊢ chaar K₀ ⊥ = 0

Tactic:
change chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}

Premises used: MeasureTheory.Measure.haar.chaar, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
this : Continuous eval
apply : clPrehaar (↑K₀ : Set G) ⊤ ⊆ eval ⁻¹' {0}
⊢ chaar K₀ ∈ eval ⁻¹' {0}

Tactic:
apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)

Premises used: Set.mem_of_subset_of_mem, Top.top, MeasureTheory.Measure.haar.chaar_mem_clPrehaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
this : Continuous eval
rw :
  prehaar (↑K₀ : Set G) '' {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
    eval ⁻¹' {0}
rw₁ : IsClosed (eval ⁻¹' {0})
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}

Tactic:
rw [IsClosed.closure_subset_iff]

Premises used: IsClosed.closure_subset_iff