awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
this : y ∈ x • (k * k⁻¹)
⊢ Membership.mem (γ := Set G) (⋃ x ∈ m, x • (k * k⁻¹)) y

Tactic:
exact mem_biUnion xm this

Premises used: Set.mem_biUnion
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
inr : ∀ (hm : m.Nonempty), 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∞)

Tactic:
rcases eq_empty_or_nonempty m with rfl | hm

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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⁻¹)
⊢ s = ∅

Tactic:
simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty, subset_empty_iff] at sm

Premises used: Set.iUnion_of_empty, Set.mem_empty_iff_false, Set.subset_empty_iff, Set.iUnion_empty
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 = ∅
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [sm]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
neg : ∀ (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∞)

Tactic:
by_cases h'm : Set.Countable m

Premises used: Set.Countable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
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∞)
⊢ 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⟩

Premises used: Set.Countable.exists_eq_range, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : ℕ
apply : ∀ (j : ℕ), MeasurableSet (f j • (k * k⁻¹))
⊢ MeasurableSet.{u_1} (α := G) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) i)

Tactic:
apply MeasurableSet.disjointed (fun j ↦ hs.inter ?_)

Premises used: MeasurableSet.disjointed, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : ℕ
⊢ IsClosed[inst] (k • k⁻¹)

Tactic:
have : IsClosed (k • k⁻¹) := IsClosed.smul_left_of_isCompact k_closed.inv k_comp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : ℕ
this : IsClosed[inst] (k • k⁻¹)
⊢ MeasurableSet (f j • (k * k⁻¹))

Tactic:
(IsClosed.smul this (f j)).measurableSet

Premises used: IsClosed.measurableSet, IsClosed.smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : ℕ
this : IsClosed[inst] (k • k⁻¹)
⊢ MeasurableSet (f j • (k * k⁻¹))

Tactic:
exact (IsClosed.smul this (f j)).measurableSet

Premises used: IsClosed.measurableSet, IsClosed.smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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)

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
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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)
⊢ s ⊆ ⋃ (y : ℕ), f y • (k * k⁻¹)

Tactic:
simp only [mem_range, iUnion_exists, iUnion_iUnion_eq'] at sm

Premises used: Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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⁻¹)
rwa₁ : s ∩ ⋃ (i : ℕ), f i • (k * k⁻¹) = s
rwa₂ rwa₃ rwa₄ rwa₅ : s ⊆ ⋃ (i : ℕ), f i • (k * k⁻¹)
⊢ s = ⋃ (n : ℕ), s ∩ f n • (k * k⁻¹)

Tactic:
rwa [← inter_iUnion, eq_comm, inter_eq_left]

Premises used: Set.inter_eq_left, eq_comm, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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⁻¹)

Tactic:
have s_eq : s = ⋃ n, s ∩ (f n • (k * k⁻¹)) := by rwa [← inter_iUnion, eq_comm, inter_eq_left]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ' : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)

Tactic:
rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]

Premises used: iUnion_disjointed, MeasureTheory.measure_iUnion, disjoint_disjointed
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)

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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)

Tactic:
rw [← measure_iUnion (disjoint_disjointed _) M, iUnion_disjointed, ← s_eq]

Premises used: iUnion_disjointed, MeasureTheory.measure_iUnion, disjoint_disjointed
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)

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]