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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₀.toCompacts
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 ⁻¹' {1}
have rw : prehaar (↑K₀ : Set G) '' {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
  eval ⁻¹' {1}
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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₀.toCompacts
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 ⁻¹' {1}
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {1}
have rw₁ : IsClosed (eval ⁻¹' {1})
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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₀.toCompacts
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 ⁻¹' {1}
have hU : (interior U).Nonempty
Tactic: apply prehaar_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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₀.toCompacts
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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₀.toCompacts
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {1})
have a : IsClosed (X := ℝ) {1}
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
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₂ - f K₁
⊢ chaar K₀ K₁ ≤ chaar K₀ K₂
have this : Continuous eval
Tactic: have : Continuous eval := (continuous_apply K₂).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
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₂ - f K₁
this : Continuous eval
⊢ chaar K₀ K₁ ≤ chaar K₀ K₂
have rw : 0 ≤ chaar K₀ K₂ - chaar K₀ K₁
Tactic: rw [← sub_nonneg]
-- 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 : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₂ - f K₁
this : Continuous eval
⊢ 0 ≤ chaar K₀ K₂ - chaar K₀ K₁
have change : chaar K₀ ∈ eval ⁻¹' Ici 0
Tactic: change chaar K₀ ∈ eval ⁻¹' Ici (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
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₂ - f K₁
this : Continuous eval
⊢ chaar K₀ ∈ eval ⁻¹' Ici 0
have apply : clPrehaar (↑K₀ : Set G) ⊤ ⊆ eval ⁻¹' Ici 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
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f 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 ⁻¹' Ici 0
have rw : prehaar (↑K₀ : Set G) '' {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
  eval ⁻¹' Ici 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 : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f 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 ⁻¹' Ici 0
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' Ici 0
have rw₁ : IsClosed (eval ⁻¹' Ici 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 : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f 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 ⁻¹' Ici 0
have simp : prehaar (↑K₀ : Set G) U K₁ ≤ prehaar (↑K₀ : Set G) U K₂
Tactic: simp only [eval, mem_preimage, mem_Ici, sub_nonneg]
-- 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 : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f 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 K₁ ≤ prehaar (↑K₀ : Set G) U K₂
have apply : (interior U).Nonempty
Tactic: apply prehaar_mono _ 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
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f 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 rw : 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 : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₂ - f K₁
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)
have a : IsClosed (X := ℝ) (Ici 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
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
⊢ chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂
have this : Continuous eval
Tactic: have : Continuous eval := by
    exact ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ 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
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂
have rw : 0 ≤ chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂)
Tactic: rw [← sub_nonneg]
-- 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ 0 ≤ chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂)
have change : chaar K₀ ∈ eval ⁻¹' Ici 0
Tactic: change chaar K₀ ∈ eval ⁻¹' Ici (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
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ chaar K₀ ∈ eval ⁻¹' Ici 0
have apply : clPrehaar (↑K₀ : Set G) ⊤ ⊆ eval ⁻¹' Ici 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
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ 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 ⁻¹' Ici 0
have rw : prehaar (↑K₀ : Set G) '' {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
  eval ⁻¹' Ici 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ 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 ⁻¹' Ici 0
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G | U ⊆ (↑(OpenNhdsOf.toOpens (x := 1) ⊤) : Set G) ∧ IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' Ici 0
have rw₁ : IsClosed (eval ⁻¹' Ici 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ 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 ⁻¹' Ici 0
have simp : prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂) ≤ prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂
Tactic: simp only [eval, mem_preimage, mem_Ici, sub_nonneg]
-- 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ 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 (K₁ ⊔ K₂) ≤ prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂
have hU : (interior U).Nonempty
Tactic: apply prehaar_sup_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
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ 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
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)
have a : IsClosed (X := ℝ) (Ici 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₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have rcases : ∀ (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₂), chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Tactic: rcases SeparatedNhds.of_isCompact_isCompact_isClosed K₁.2 K₂.2 h₂ h
    with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, 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₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have rcases : ∀ (L₁ : Set G) (h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁) (h2L₁ : K₁.carrier * L₁ ⊆ U₁),
  chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Tactic: rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, 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₁
h2L₁ : K₁.carrier * L₁ ⊆ U₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have rcases : ∀ (V₁ : Set G) (h1V₁ : V₁ ⊆ L₁) (h2V₁ : IsOpen[inst_1] V₁) (h3V₁ : 1 ∈ V₁),
  chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Tactic: rcases mem_nhds_iff.mp h1L₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩
-- 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
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₁
h2L₁ : K₁.carrier * L₁ ⊆ U₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have h2L₂ : K₁.carrier * V₁ ⊆ U₁
Tactic: replace h2L₁ := Subset.trans (mul_subset_mul_left h1V₁) h2L₁
Cleared hypotheses: 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₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have rcases : ∀ (L₂ : Set G) (h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂) (h2L₂ : K₂.carrier * L₂ ⊆ U₂),
  chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Tactic: rcases compact_open_separated_mul_right K₂.2 h1U₂ h2U₂ with ⟨L₂, h1L₂, 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₂
h2L₂ : K₂.carrier * L₂ ⊆ U₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have rcases : ∀ (V₂ : Set G) (h1V₂ : V₂ ⊆ L₂) (h2V₂ : IsOpen[inst_1] V₂) (h3V₂ : 1 ∈ V₂),
  chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Tactic: rcases mem_nhds_iff.mp h1L₂ with ⟨V₂, h1V₂, h2V₂, h3V₂⟩
-- 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
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₂
h2L₂ : K₂.carrier * L₂ ⊆ U₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have h2L₃ : K₂.carrier * V₂ ⊆ U₂
Tactic: replace h2L₂ := Subset.trans (mul_subset_mul_left h1V₂) h2L₂
Cleared hypotheses: h2L₂
-- 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
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₂)
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have this : Continuous eval
Tactic: have : Continuous eval :=
    ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ 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
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
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
have rw : chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂) = 0
Tactic: rw [eq_comm, ← 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
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
⊢ chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (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
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₂
⊢ chaar K₀ ∈ eval ⁻¹' {0}
have mem_of_subset_of_mem : clPrehaar (↑K₀ : Set G) { carrier := V⁻¹, is_open' := sorry, mem' := sorry : OpenNhdsOf (α := G) 1 } ⊆ eval ⁻¹' {0}
Tactic: apply
    mem_of_subset_of_mem _
      (chaar_mem_clPrehaar K₀
        ⟨⟨V⁻¹, (h2V₁.inter h2V₂).preimage continuous_inv⟩, by
          simp only [V, mem_inv, inv_one, h3V₁, h3V₂, mem_inter_iff, true_and]⟩)
-- 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₂
⊢ 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 : prehaar (↑K₀ : Set G) ''
    {U : Set G |
      U ⊆ (↑{ carrier := V⁻¹, is_open' := sorry, mem' := sorry : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧
        IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
  eval ⁻¹' {0}
Tactic: rw [IsClosed.closure_subset_iff]