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 : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index ((fun (h : G) ↦ g * h) '' K) V = index K V
have refine : index K V ≤ index ((fun (h : G) ↦ g * h) '' K) V
Tactic: refine le_antisymm (mul_left_index_le hK hV g) ?_
-- 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 : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index K V ≤ index ((fun (h : G) ↦ g * h) '' K) V
have h : K = (fun (h : G) ↦ g⁻¹ * h) '' (fun (x : G) ↦ g * x) '' K
Tactic: convert! mul_left_index_le (hK.image <| continuous_const_mul g) hV g⁻¹
-- 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 : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun (h : G) ↦ g⁻¹ * h) '' (fun (x : G) ↦ g * x) '' K
have h : K = (fun (x : G) ↦ g⁻¹ * (g * x)) '' K
Tactic: rw [image_image]
-- 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
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑K : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)
have rw : (↑(index (↑K : Set G) U) : ℝ) ≤
  HMul.hMul (α := ℝ) (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
Tactic: rw [div_le_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
U : Set G
K : Compacts G
hU : (interior U).Nonempty
rw :
  (↑(index (↑K : Set G) U) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑K : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)
have rw₁ : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
Tactic: rw [div_le_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
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ (↑(index (↑K : Set G) U) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
have norm_cast : index (↑K : Set G) U ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) U
Tactic: norm_cast
-- 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
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
have norm_cast : 0 < index (↑K₀ : Set G) U
Tactic: norm_cast
-- 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
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := h1K : Compacts G }
have ha : LT.lt (α := ℝ) 0 (↑(index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U) : ℝ)
Tactic: apply div_pos
-- 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
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
ha : LT.lt (α := ℝ) 0 (↑(index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U) : ℝ)
⊢ 0 < prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := h1K : Compacts G }
have hb : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
Tactic: apply div_pos
-- 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
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U) : ℝ)
have ha : 0 < index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U
Tactic: norm_cast
-- 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
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
have hb : 0 < index (↑K₀ : Set G) U
Tactic: norm_cast
-- 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
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
have rw : LE.le (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
Tactic: rw [div_le_div_iff_of_pos_right]
-- 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
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
rw : LE.le (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
have rw₁ : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
Tactic: rw [div_le_div_iff_of_pos_right]
-- 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
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
have rw : (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
Tactic: rw [← add_div, div_le_div_iff_of_pos_right]
-- 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
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
rw :
  (↑(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) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
have rw₁ : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
Tactic: rw [← add_div, div_le_div_iff_of_pos_right]
-- 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
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) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
have rw : 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: rw [← add_div]
-- 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
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) : ℝ)
have refine : (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) = HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
Tactic: refine congr_arg (fun x : ℝ => x / index K₀ U) ?_
-- 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
⊢ IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
have h : ∀ (i : Compacts G), IsCompact (X := ℝ) (Icc 0 (↑(index (↑i : Set G) (↑K₀ : Set G)) : ℝ))
Tactic: apply isCompact_univ_pi
-- 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
⊢ Set.Nonempty (α := Compacts G → ℝ)
    (haarProduct (↑K₀ : Set G) ∩ ⋂ (V : OpenNhdsOf (α := G) 1), clPrehaar (↑K₀ : Set G) V)
have this : 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
-- 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
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)
have refine : ∀ (t : Finset (OpenNhdsOf (α := G) 1)),
  Set.Nonempty (α := Compacts G → ℝ) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
Tactic: refine this.inter_iInter_nonempty (clPrehaar K₀) (fun s => isClosed_closure) fun t => ?_
-- 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
this : IsCompact (X := Compacts G → ℝ) (haarProduct (↑K₀ : Set G))
t : Finset (OpenNhdsOf (α := G) 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
⊢ Set.Nonempty (α := Compacts G → ℝ) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
have h1V₀ : IsOpen[inst_1] V₀
Tactic: have h1V₀ : IsOpen V₀ := isOpen_biInter_finset <| by rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₁
-- 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
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₀
have simp : ∀ (i : OpenNhdsOf (α := G) 1) (i_1 : i ∈ t), 1 ∈ i.carrier
Tactic: simp only [V₀, mem_iInter]
-- 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
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₀
⊢ Set.Nonempty (α := Compacts G → ℝ) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
have h2V₀ : 1 ∈ V₀
Tactic: have h2V₀ : (1 : G) ∈ V₀ := by simp only [V₀, mem_iInter]; rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₂
-- 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
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)
have refine : Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
  (prehaar (↑K₀ : Set G) V₀)
Tactic: refine ⟨prehaar K₀ V₀, ?_⟩
-- 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
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₀
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
    (prehaar (↑K₀ : Set G) V₀)
have left : Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G)) (prehaar (↑K₀ : Set G) V₀)
Tactic: constructor
-- 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
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₀)
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G) ∩ ⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i)
    (prehaar (↑K₀ : Set G) V₀)
have right : Membership.mem (γ := Set (Compacts G → ℝ)) (⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i) (prehaar (↑K₀ : Set G) V₀)
Tactic: constructor
-- 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
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₀
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct (↑K₀ : Set G)) (prehaar (↑K₀ : Set G) V₀)
have left : (interior V₀).Nonempty
Tactic: apply prehaar_mem_haarProduct 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
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₀
⊢ (interior V₀).Nonempty
have h : 1 ∈ interior V₀
Tactic: use 1
-- 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
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₀
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (⋂ i ∈ t, clPrehaar (↑K₀ : Set G) i) (prehaar (↑K₀ : Set G) V₀)
have right : ∀ (i : OpenNhdsOf (α := G) 1) (i_1 : i ∈ t), prehaar (↑K₀ : Set G) V₀ ∈ clPrehaar (↑K₀ : Set G) i
Tactic: simp only [mem_iInter]
-- 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
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
⊢ prehaar (↑K₀ : Set G) V₀ ∈ clPrehaar (↑K₀ : Set G) { toOpens := V, mem' := hV : OpenNhdsOf (α := G) 1 }
have 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₀)
Tactic: apply subset_closure
-- 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
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
⊢ 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₀)
have 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₀
Tactic: apply mem_image_of_mem
-- 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
V : OpenNhdsOf (α := G) 1
⊢ chaar K₀ ∈ clPrehaar (↑K₀ : Set G) V
have 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))
    sorry)
Tactic: have := (Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).2
-- 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
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))
      ⋯)
⊢ chaar K₀ ∈ clPrehaar (↑K₀ : Set G) V
have 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))
      sorry ∈
    clPrehaar (↑K₀ : Set G) i
Tactic: rw [mem_iInter] at this
Cleared hypotheses: 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 : Compacts G
⊢ 0 ≤ chaar K₀ K
have 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)
Tactic: have := chaar_mem_haarProduct K₀ K (mem_univ _)
-- 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 : 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
have this₁ : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)
Tactic: rw [mem_Icc] at this
Cleared hypotheses: 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
⊢ chaar K₀ ⊥ = 0
have this : Continuous eval
Tactic: have : Continuous eval := continuous_apply ⊥
-- 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 ⊥
this : Continuous eval
⊢ chaar 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
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
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}
⊢ 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
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f ⊥
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 (hypothesis)
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
⊢ chaar K₀ K₀.toCompacts = 1
have this : Continuous eval
Tactic: have : Continuous eval := continuous_apply _
-- 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
⊢ chaar K₀ K₀.toCompacts = 1
have change : chaar K₀ ∈ eval ⁻¹' {1}
Tactic: change chaar K₀ ∈ eval ⁻¹' {(1 : ℝ)}
-- 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
⊢ chaar K₀ ∈ eval ⁻¹' {1}
have apply : clPrehaar (↑K₀ : Set G) ⊤ ⊆ eval ⁻¹' {1}
Tactic: apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)