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}
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∞)
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))
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [I, J]
-- 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∞)
J :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (ν : (a : Set G) → ℝ≥0∞) (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n) : ℝ≥0∞)
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∞)
⊢ 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:
congr with n
-- 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∞)
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 : ℕ
pos : IsCompact.{u_1} (X := G) (closure[inst] (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) 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:
apply measure_isMulInvariant_eq_smul_of_isCompact_closure

Premises used: MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure
-- 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∞)
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 (f n • (k * k⁻¹))

Tactic:
have : IsCompact (f n • (k * k⁻¹)) := IsCompact.smul (f n) (k_comp.mul k_comp.inv)
-- 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∞)
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 : ℕ
this : IsCompact (f n • (k * k⁻¹))
⊢ IsCompact.{u_1} (X := G) (closure[inst] (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))

Tactic:
this.closure_of_subset <| (disjointed_subset _ _).trans inter_subset_right

Premises used: HasSubset.Subset.trans, disjointed_subset, IsCompact.closure_of_subset, Set.inter_subset_right
-- 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∞)
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 : ℕ
this : IsCompact (f n • (k * k⁻¹))
⊢ IsCompact.{u_1} (X := G) (closure[inst] (disjointed (fun (n : ℕ) ↦ s ∩ f n • (k * k⁻¹)) n))

Tactic:
exact this.closure_of_subset <| (disjointed_subset _ _).trans inter_subset_right

Premises used: HasSubset.Subset.trans, disjointed_subset, IsCompact.closure_of_subset, Set.inter_subset_right
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
⊢ ∀ (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
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
contrapose! : ∀ (h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), m.Countable
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
contrapose! h'm
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : Pairwise.{u_1} (α := (↑m : Type u_1)) (onFun (β := Set G) Disjoint fun (i : (↑m : Type u_1)) ↦ s ∩ (↑i : G) • k)
apply₁ : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) (⋃ (i : (↑m : Type u_1)), s ∩ (↑i : G) • k) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (∑' (x : (↑m : Type u_1)), (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑x : G) • k)) ∞

Tactic:
apply lt_of_le_of_lt (MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint _ M _) _

Premises used: lt_of_le_of_lt, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ s ∩ x • k

Tactic:
have I : PairwiseDisjoint m fun x ↦ s ∩ x • k :=
            hdj.mono (fun x ↦ inter_subset_right)
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ s ∩ x • k
⊢ Pairwise.{u_1} (α := (↑m : Type u_1)) (onFun (β := Set G) Disjoint fun (i : (↑m : Type u_1)) ↦ s ∩ (↑i : G) • k)

Tactic:
I.on_injective Subtype.val_injective (fun x ↦ x.2)

Premises used: Subtype.val_injective, Set.Pairwise.on_injective, Subtype.property
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ s ∩ x • k
⊢ Pairwise.{u_1} (α := (↑m : Type u_1)) (onFun (β := Set G) Disjoint fun (i : (↑m : Type u_1)) ↦ s ∩ (↑i : G) • k)

Tactic:
exact I.on_injective Subtype.val_injective (fun x ↦ x.2)

Premises used: Subtype.val_injective, Set.Pairwise.on_injective, Subtype.property
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ⋃ (i : (↑m : Type u_1)), s ∩ (↑i : G) • k ⊆ s

Tactic:
simp [inter_subset_left]

Premises used: Set.inter_subset_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}
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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) (⋃ (i : (↑m : Type u_1)), s ∩ (↑i : G) • k) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact lt_of_le_of_lt (measure_mono (by simp [inter_subset_left])) h'm.lt_top

Premises used: lt_of_le_of_lt, Ne.lt_top, MeasureTheory.measure_mono
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (∑' (x : (↑m : Type u_1)), (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑x : G) • k)) ∞

Tactic:
have : ∑' (x : m), ρ (s ∩ ((x : G) • k)) < ∞ := by
        apply lt_of_le_of_lt (MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint _ M _) _
        · have I : PairwiseDisjoint m fun x ↦ s ∩ x • k :=
            hdj.mono (fun x ↦ inter_subset_right)
          exact I.on_injective Subtype.val_injective (fun x ↦ x.2)
        · exact lt_of_le_of_lt (measure_mono (by simp [inter_subset_left])) h'm.lt_top
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (∑' (x : (↑m : Type u_1)), (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑x : G) • k)) ∞
⊢ Set.Countable.{u_1} (α := (↑m : Type u_1))
    (support (M := ℝ≥0∞) fun (i : (↑m : Type u_1)) ↦ (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑i : G) • k))

Tactic:
have C : Set.Countable (support fun (i : m) ↦ ρ (s ∩ (i : G) • k)) :=
        Summable.countable_support_ennreal this.ne
-- 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
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : (↑m : Type u_1)), MeasurableSet (s ∩ (↑i : G) • k)
h'm : Ne (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (∑' (x : (↑m : Type u_1)), (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑x : G) • k)) ∞
C :
  Set.Countable.{u_1} (α := (↑m : Type u_1))
    (support (M := ℝ≥0∞) fun (i : (↑m : Type u_1)) ↦ (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑i : G) • k))
⊢ Eq.{u_1 + 1} (α := Set (↑m : Type u_1))
    (support (M := ℝ≥0∞) fun (i : (↑m : Type u_1)) ↦ (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑i : G) • k)) univ

Tactic:
eq_univ_iff_forall.2 fun i ↦ ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall