awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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₂
rw :
  prehaar (↑K₀ : Set G) ''
      {U : Set G |
        U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧
          IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
    eval ⁻¹' {0}
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G |
          U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧
            IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}
have rw₁ : IsClosed (eval ⁻¹' {0})
Tactic: rw [IsClosed.closure_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U ∈ eval ⁻¹' {0}
have simp : prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂ = prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂)
Tactic: simp only [eval, mem_preimage, sub_eq_zero, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂ = prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂)
have rw : prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂
have hU₁ : (interior U).Nonempty
Tactic: apply prehaar_sup_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
hU₁ : (interior U).Nonempty
⊢ prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂
have h₁ : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
Tactic: apply prehaar_sup_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ (interior U).Nonempty
have hU₁ : U.Nonempty
Tactic: rw [h2U.interior_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
have h₁ : K₁.carrier * U⁻¹ ⊆ U₁
Tactic: refine disjoint_of_subset ?_ ?_ hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
h₁ : K₁.carrier * U⁻¹ ⊆ U₁
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
have h₃ : K₂.carrier * U⁻¹ ⊆ U₂
Tactic: refine disjoint_of_subset ?_ ?_ hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ K₁.carrier * U⁻¹ ⊆ U₁
have h₁ : U⁻¹ ⊆ V₁
Tactic: refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ K₂.carrier * U⁻¹ ⊆ U₂
have h₁ : U⁻¹ ⊆ V₂
Tactic: refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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 (eval ⁻¹' {0})
have a : IsClosed (X := ℝ) {0}
Tactic: apply continuous_iff_isClosed.mp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
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
⊢ chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = chaar K₀ K
have this : Continuous eval
Tactic: have : Continuous eval := (continuous_apply (K.map _ _)).sub (continuous_apply K)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = chaar K₀ K
have rw : chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) sorry K) - chaar K₀ K = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ chaar K₀ (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) - chaar K₀ K = 0
have change : chaar K₀ ∈ eval ⁻¹' {0}
Tactic: change chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ chaar K₀ ∈ eval ⁻¹' {0}
have apply : clPrehaar (↑K₀ : Set G) ⊤ ⊆ eval ⁻¹' {0}
Tactic: apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}
have rw : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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}
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}
have rw₁ : IsClosed (eval ⁻¹' {0})
Tactic: rw [IsClosed.closure_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U ∈ eval ⁻¹' {0}
have simp : prehaar (↑K₀ : Set G) U (Compacts.map (fun (x : G) ↦ g * x) sorry K) = prehaar (↑K₀ : Set G) U K
Tactic: simp only [eval, mem_singleton_iff, mem_preimage, sub_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) = prehaar (↑K₀ : Set G) U K
have hU : (interior U).Nonempty
Tactic: apply is_left_invariant_prehaar
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ (interior U).Nonempty
have hU : U.Nonempty
Tactic: rw [h2U.interior_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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 (eval ⁻¹' {0})
have a : IsClosed (X := ℝ) {0}
Tactic: apply continuous_iff_isClosed.mp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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₁ ⊔ K₂)) ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) ⋯ + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) ⋯
have simp : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁ + chaar K₀ K₂) sorry =
  Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₁) sorry + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (chaar K₀ K₂) sorry
Tactic: simp only [chaar_sup_eq h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ Eq (α := ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K₀.toCompacts : ℝ≥0∞) (1 : ℝ≥0∞)
have simp_rw : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 1 sorry = 1
Tactic: simp_rw [← ENNReal.coe_one, haarContent_apply, ENNReal.coe_inj, chaar_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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∞)
have refine : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)
Tactic: refine zero_lt_one.trans_le ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞)
have 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 })
Tactic: rw [Content.outerMeasure_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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 })
have 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∞)
Tactic: refine le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans ?_ <| le_iSup₂ K₀.toCompacts hK₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ IsMulLeftInvariant (haarMeasure K₀)
have 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∞)
Tactic: rw [← forall_measure_preimage_mul_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 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∞)
have 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∞)
Tactic: rw [haarMeasure_apply hA, haarMeasure_apply (measurable_const_mul g hA)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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∞)
have 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∞)
Tactic: refine congr_arg (fun x : ℝ≥0∞ => x / (haarContent K₀).measure K₀) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 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∞)
have h : ∀ (g : G) {K : Compacts G},
  Eq (α := ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) sorry K) : ℝ≥0∞)
    ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: apply Content.is_mul_left_invariant_outerMeasure