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
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₂

Tactic:
Subset.trans (inv_subset.mpr h1U) inter_subset_right

Premises used: Iff.mpr, Set.Subset.trans, Set.inv_subset, Set.inter_subset_right
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₂

Tactic:
exact Subset.trans (inv_subset.mpr h1U) inter_subset_right

Premises used: Iff.mpr, Set.Subset.trans, Set.inv_subset, Set.inter_subset_right
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
a : IsClosed (X := ℝ) {0}
⊢ IsClosed (eval ⁻¹' {0})

Tactic:
apply continuous_iff_isClosed.mp this

Premises used: continuous_iff_isClosed, Iff.mp
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ IsClosed (X := ℝ) {0}

Tactic:
isClosed_singleton

Premises used: isClosed_singleton
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ IsClosed (X := ℝ) {0}

Tactic:
exact isClosed_singleton

Premises used: isClosed_singleton
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
⊢ Continuous eval

Tactic:
have : Continuous eval := (continuous_apply (K.map _ _)).sub (continuous_apply K)
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
rw : chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - chaar K₀ K = 0
⊢ chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = chaar K₀ K

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
change : chaar K₀ ∈ eval ⁻¹' {0}
⊢ chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - chaar K₀ 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
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
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
U : Set G
left : U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
simp : prehaar (↑K₀ : Set G) U (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = prehaar (↑K₀ : Set G) U K
⊢ prehaar (↑K₀ : Set G) U ∈ eval ⁻¹' {0}

Tactic:
simp only [eval, mem_singleton_iff, mem_preimage, sub_eq_zero]

Premises used: sub_eq_zero, Set.mem_singleton_iff, Set.mem_preimage
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
U : Set G
left : U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
hU : (interior U).Nonempty
⊢ prehaar (↑K₀ : Set G) U (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = prehaar (↑K₀ : Set G) U K

Tactic:
apply is_left_invariant_prehaar

Premises used: MeasureTheory.Measure.haar.is_left_invariant_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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
U : Set G
left : U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
hU : U.Nonempty
⊢ (interior U).Nonempty

Tactic:
rw [h2U.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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
U : Set G
left : U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U.Nonempty

Tactic:
⟨1, h3U⟩

Premises used: Set.Nonempty, Exists.intro, 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
U : Set G
left : U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U.Nonempty

Tactic:
exact ⟨1, h3U⟩
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
a : IsClosed (X := ℝ) {0}
⊢ IsClosed (eval ⁻¹' {0})

Tactic:
apply continuous_iff_isClosed.mp this

Premises used: continuous_iff_isClosed, Iff.mp
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ IsClosed (X := ℝ) {0}

Tactic:
isClosed_singleton

Premises used: isClosed_singleton
-- 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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ IsClosed (X := ℝ) {0}

Tactic:
exact isClosed_singleton

Premises used: isClosed_singleton
-- 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₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) ⋯ ≤ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) ⋯

Tactic:
simp only [← NNReal.coe_le_coe, NNReal.toReal, chaar_mono, h]

Premises used: MeasureTheory.Measure.haar.chaar_mono, NNReal.toReal, NNReal.coe_le_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
K₁ K₂ : Compacts G
h : Disjoint (↑K₁ : Set G) (↑K₂ : Set G)
_h₁ : IsClosed[inst_1] (↑K₁ : Set G)
h₂ : IsClosed[inst_1] (↑K₂ : Set G)
simp :
  Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁ + chaar K₀ K₂) ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) ⋯ + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) ⋯
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ (K₁ ⊔ K₂)) ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) ⋯ + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) ⋯

Tactic:
simp only [chaar_sup_eq h]

Premises used: MeasureTheory.Measure.haar.chaar_sup_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
K₁ K₂ : Compacts G
h : Disjoint (↑K₁ : Set G) (↑K₂ : Set G)
_h₁ : IsClosed[inst_1] (↑K₁ : Set G)
h₂ : IsClosed[inst_1] (↑K₂ : Set G)
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁ + chaar K₀ K₂) ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) ⋯ + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) ⋯

Tactic:
rfl
-- 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₁ K₂ : Compacts G
⊢ (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ (K₁ ⊔ K₂)) ⋯) : ℝ) ≤
    (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) ⋯) : ℝ) +
      (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) ⋯) : ℝ)

Tactic:
simp only [NNReal.toReal, chaar_sup_le]

Premises used: MeasureTheory.Measure.haar.chaar_sup_le, NNReal.toReal
-- 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
⊢ (haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K =
    (↑(have this := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K) ⋯;
        this) :
      ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- 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
simp_rw : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 1 ⋯ = 1
⊢ Eq (α := ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K₀.toCompacts : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp_rw [← ENNReal.coe_one, haarContent_apply, ENNReal.coe_inj, chaar_self]

Premises used: ENNReal.coe_inj, ENNReal.coe_one, MeasureTheory.Measure.haar.haarContent_apply, MeasureTheory.Measure.haar.chaar_self
-- 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
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 1 ⋯ = 1

Tactic:
rfl
-- 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
g : G
K : Compacts G
⊢ Eq (α := ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
    ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
simpa only [ENNReal.coe_inj, ← NNReal.coe_inj, haarContent_apply] using
    is_left_invariant_chaar g K

Premises used: ENNReal.coe_inj, MeasureTheory.Measure.haar.haarContent_apply, MeasureTheory.Measure.haar.is_left_invariant_chaar, NNReal.coe_inj
-- 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
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)

Tactic:
zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- 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
refine : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)

Tactic:
refine zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- 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
rw :
  LE.le (α := ℝ≥0∞) 1
    (⨅ (U : Set G),
      ⨅ (hU : IsOpen[inst_1] U),
        ⨅ (_ : (↑K₀ : Set G) ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU })
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)

Tactic:
rw [Content.outerMeasure_eq_iInf]

Premises used: MeasureTheory.Content.outerMeasure_eq_iInf
-- 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
⊢ LE.le (α := ℝ≥0∞) 1
    (⨅ (U : Set G),
      ⨅ (hU : IsOpen[inst_1] U),
        ⨅ (_ : (↑K₀ : Set G) ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU })

Tactic:
le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans ?_ <| le_iSup₂ K₀.toCompacts hK₀

Premises used: le_iSup₂, le_iInf, TopologicalSpace.PositiveCompacts.toCompacts, le_iInf₂, le_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
refine :
  ∀ (U : Set G) (hU : IsOpen[inst_1] U) (hK₀ : (↑K₀ : Set G) ⊆ U),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K₀.toCompacts : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) 1
    (⨅ (U : Set G),
      ⨅ (hU : IsOpen[inst_1] U),
        ⨅ (_ : (↑K₀ : Set G) ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU })

Tactic:
refine le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans ?_ <| le_iSup₂ K₀.toCompacts hK₀

Premises used: le_iSup₂, le_iInf, TopologicalSpace.PositiveCompacts.toCompacts, le_iInf₂, le_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
hU : IsOpen[inst_1] U
hK₀ : (↑K₀ : Set G) ⊆ U
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K₀.toCompacts : ℝ≥0∞)

Tactic:
haarContent_self.ge

Premises used: Eq.ge, MeasureTheory.Measure.haar.haarContent_self
-- 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 : IsOpen[inst_1] U
hK₀ : (↑K₀ : Set G) ⊆ U
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K₀.toCompacts : ℝ≥0∞)

Tactic:
exact haarContent_self.ge

Premises used: Eq.ge, MeasureTheory.Measure.haar.haarContent_self
-- 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
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)

Tactic:
(haarContent_outerMeasure_self_pos K₀).trans_le (OuterMeasure.mono _ subset_closure)

Premises used: subset_closure, MeasureTheory.OuterMeasure.mono, LT.lt.trans_le, MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
s : Set G
hs : MeasurableSet s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)

Tactic:
simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]

Premises used: div_eq_mul_inv, mul_comm, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
rw :
  ∀ (g : G) (A : Set G),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
        (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ IsMulLeftInvariant (haarMeasure K₀)

Tactic:
rw [← forall_measure_preimage_mul_iff]

Premises used: MeasureTheory.forall_measure_preimage_mul_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
rw :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
    (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [haarMeasure_apply hA, haarMeasure_apply (measurable_const_mul g hA)]

Premises used: MeasureTheory.Measure.haarMeasure_apply, MeasurableMul.measurable_const_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)

Tactic:
congr_arg (fun x : ℝ≥0∞ => x / (haarContent K₀).measure K₀) ?_

Premises used: HDiv.hDiv, congr_arg, SetLike.coe, MeasureTheory.Content.measure, MeasureTheory.Measure.haar.haarContent, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
refine :
  Eq (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞)
    (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)

Tactic:
refine congr_arg (fun x : ℝ≥0∞ => x / (haarContent K₀).measure K₀) ?_

Premises used: HDiv.hDiv, congr_arg, SetLike.coe, MeasureTheory.Content.measure, MeasureTheory.Measure.haar.haarContent, DFunLike.coe