awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
⊢ s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
have rwa : s = s ∩ ⋃ (i : ℕ), f i • (k * k⁻¹)
Tactic: rwa [← inter_iUnion, eq_comm, inter_eq_left]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
rwa : s = s ∩ ⋃ (i : ℕ), f i • (k * k⁻¹)
⊢ s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
have rwa₁ : s ∩ ⋃ (i : ℕ), f i • (k * k⁻¹) = s
Tactic: rwa [← inter_iUnion, eq_comm, inter_eq_left]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
Tactic: have s_eq : s = ⋃ n, s ∩ (f n • (k * k⁻¹)) := by rwa [← inter_iUnion, eq_comm, inter_eq_left]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ' : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
rw :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i • (k * k⁻¹)) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
rw :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i • (k * k⁻¹)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have I : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
  (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
Tactic: have I : μ' s = ∑' n, μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n) := by
      rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i • (k * k⁻¹)) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i • (k * k⁻¹)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have J : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
  (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
Tactic: have J : ν s = ∑' n, ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n) := by
      rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
J :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))
  (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))
Tactic: rw [I, J]
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
J :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))
have pos : ∀ (n : ℕ),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
Tactic: congr with n
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
J :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
have pos : IsCompact.{u_1} (X := G) (closure[inst] (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))
Tactic: apply measure_isMulInvariant_eq_smul_of_isCompact_closure
-- 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
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)
s_eq : s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)
I :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
J :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
n : ℕ
⊢ IsCompact.{u_1} (X := G) (closure[inst] (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))
have this : IsCompact (f n • (k * k⁻¹))
Tactic: have : IsCompact (f n • (k * k⁻¹)) := IsCompact.smul (f n) (k_comp.mul k_comp.inv)
-- 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
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
ρ : Measure G
hρ : ρ.IsEverywherePos s
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
Tactic: have M : ∀ (i : ↑m), MeasurableSet (s ∩ (i : G) • k) :=
        fun i ↦ hs.inter (IsClosed.smul k_closed _).measurableSet