awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have hms : m ⊆ s
Tactic: obtain ⟨hms : m ⊆ s, hdj : PairwiseDisjoint m (fun x ↦ x • k)⟩ := m_max.prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
Tactic: obtain ⟨hms : m ⊆ s, hdj : PairwiseDisjoint m (fun x ↦ x • k)⟩ := m_max.prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
have pos : ∀ (h'y : m ∪ {y} ∈ A), Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
Tactic: by_cases h'y : m ∪ {y} ∈ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
pos : ∀ (h'y : m ∪ {y} ∈ A), Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
have neg : ∀ (h'y : m ∪ {y} ∉ A), Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
Tactic: by_cases h'y : m ∪ {y} ∈ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
have ym : y ∈ m
Tactic: have ym : y ∈ m := m_max.mem_of_prop_insert (by simpa using h'y)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
ym : y ∈ m
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
have this : y ∈ y • (k * k⁻¹)
Tactic: have : y ∈ y • (k * k⁻¹) := by
        simpa using mem_leftCoset y (Set.mul_mem_mul one_k (Set.inv_mem_inv.mpr one_k))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
have neg : ∀ (x : G) (xm : x ∈ m) (z : G) (zy : z ∈ y • k) (zx : z ∈ x • k), Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
Tactic: obtain ⟨x, xm, -, z, zy, zx⟩ : ∃ x ∈ m, y ≠ x ∧ ∃ z, z ∈ y • k ∧ z ∈ x • k := by
        simpa [A, hms, hy, insert_subset_iff, pairwiseDisjoint_insert, hdj, not_disjoint_iff]
          using h'y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ y ∈ x • (k * k⁻¹)
have rw : x * (x⁻¹ * z * (y⁻¹ * z)⁻¹) ∈ x • (k * k⁻¹)
Tactic: rw [show y = x * ((x⁻¹ * z) * (y⁻¹ * z)⁻¹) by group]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ x * (x⁻¹ * z * (y⁻¹ * z)⁻¹) ∈ x • (k * k⁻¹)
have this : x⁻¹ * z * (y⁻¹ * z)⁻¹ ∈ k * k⁻¹
Tactic: have : (x⁻¹ * z) * (y⁻¹ * z)⁻¹ ∈ k * k⁻¹ := Set.mul_mem_mul ((mem_leftCoset_iff x).mp zx)
          (Set.inv_mem_inv.mpr ((mem_leftCoset_iff y).mp zy))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y
have this : y ∈ x • (k * k⁻¹)
Tactic: have : y ∈ x • (k * k⁻¹) := by
        rw [show y = x * ((x⁻¹ * z) * (y⁻¹ * z)⁻¹) by group]
        have : (x⁻¹ * z) * (y⁻¹ * z)⁻¹ ∈ k * k⁻¹ := Set.mul_mem_mul ((mem_leftCoset_iff x).mp zx)
          (Set.inv_mem_inv.mpr ((mem_leftCoset_iff y).mp zy))
        exact mem_leftCoset x this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
Tactic: have sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹) := by
    intro y hy
    by_cases h'y : m ∪ {y} ∈ A
    · have ym : y ∈ m := m_max.mem_of_prop_insert (by simpa using h'y)
      have : y ∈ y • (k * k⁻¹) := by
        simpa using mem_leftCoset y (Set.mul_mem_mul one_k (Set.inv_mem_inv.mpr one_k))
      exact mem_biUnion ym this
    · obtain ⟨x, xm, -, z, zy, zx⟩ : ∃ x ∈ m, y ≠ x ∧ ∃ z, z ∈ y • k ∧ z ∈ x • k := by
        simpa [A, hms, hy, insert_subset_iff, pairwiseDisjoint_insert, hdj, not_disjoint_iff]
          using h'y
      have : y ∈ x • (k * k⁻¹) := by
        rw [show y = x * ((x⁻¹ * z) * (y⁻¹ * z)⁻¹) by group]
        have : (x⁻¹ * z) * (y⁻¹ * z)⁻¹ ∈ k * k⁻¹ := Set.mul_mem_mul ((mem_leftCoset_iff x).mp zx)
          (Set.inv_mem_inv.mpr ((mem_leftCoset_iff y).mp zy))
        exact mem_leftCoset x this
      exact mem_biUnion xm this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have inl : ∀ (m_max : Maximal (fun (x : Set G) ↦ x ∈ A) ∅) (hms : ∅ ⊆ s)
  (hdj : PairwiseDisjoint (α := Set G) ∅ fun (x : G) ↦ x • k)
  (sm : s ⊆ ⋃ (x : G), ⋃ (_ : Membership.mem (γ := Set G) ∅ x), x • (k * k⁻¹)),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty m with rfl | hm
Cleared hypotheses: m, m_max, hms, hdj, sm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
inl :
  ∀ (m_max : Maximal (fun (x : Set G) ↦ x ∈ A) ∅) (hms : ∅ ⊆ s)
    (hdj : PairwiseDisjoint (α := Set G) ∅ fun (x : G) ↦ x • k)
    (sm : s ⊆ ⋃ (x : G), ⋃ (_ : Membership.mem (γ := Set G) ∅ x), x • (k * k⁻¹)),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ∀ (hm : m.Nonempty), Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty m with rfl | hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) ∅
hms : ∅ ⊆ s
hdj : PairwiseDisjoint (α := Set G) ∅ fun (x : G) ↦ x • k
sm : s ⊆ ⋃ (x : G), ⋃ (_ : Membership.mem (γ := Set G) ∅ x), x • (k * k⁻¹)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have sm₁ : s = ∅
Tactic: simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty, subset_empty_iff] at sm
Cleared hypotheses: sm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (h'm : m.Countable), Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases h'm : Set.Countable m
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
pos : ∀ (h'm : m.Countable), Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (h'm : ¬m.Countable), Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases h'm : Set.Countable m
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : m.Countable
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (f : ℕ → G) (m_max : Maximal (fun (x : Set G) ↦ x ∈ A) (range f)) (hms : range f ⊆ s)
  (hdj : (range f).PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k) (sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹))
  (hm : (range f).Nonempty) (h'm : (range f).Countable),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases h'm.exists_eq_range hm with ⟨f, rfl⟩
Cleared hypotheses: m, m_max, hms, hdj, sm, hm, h'm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
f : ℕ → G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹)
hm : (range f).Nonempty
h'm : (range f).Countable
i : ℕ
⊢ MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
have apply : ∀ (j : ℕ), MeasurableSet (f j • (k * k⁻¹))
Tactic: apply MeasurableSet.disjointed (fun j ↦ hs.inter ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
f : ℕ → G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹)
hm : (range f).Nonempty
h'm : (range f).Countable
i j : ℕ
⊢ MeasurableSet (f j • (k * k⁻¹))
have this : IsClosed[inst] (k • k⁻¹)
Tactic: have : IsClosed (k • k⁻¹) := IsClosed.smul_left_of_isCompact k_closed.inv k_comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
f : ℕ → G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹)
hm : (range f).Nonempty
h'm : (range f).Countable
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
Tactic: have M i : MeasurableSet (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) i) := by
      apply MeasurableSet.disjointed (fun j ↦ hs.inter ?_)
      have : IsClosed (k • k⁻¹) := IsClosed.smul_left_of_isCompact k_closed.inv k_comp
      exact (IsClosed.smul this (f j)).measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
f : ℕ → G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹)
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have sm₁ : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
Tactic: simp only [mem_range, iUnion_exists, iUnion_iUnion_eq'] at sm
Cleared hypotheses: sm