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
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))
refine :
  ∀ (i : (↑m : Type u_1)),
    Membership.mem (γ := Set (↑m : Type u_1))
      (support (M := ℝ≥0∞) fun (i : (↑m : Type u_1)) ↦ (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑i : G) • k)) i
⊢ 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:
refine eq_univ_iff_forall.2 fun i ↦ ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- 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))
i : (↑m : Type u_1)
⊢ Membership.mem (γ := Set (↑m : Type u_1))
    (support (M := ℝ≥0∞) fun (i : (↑m : Type u_1)) ↦ (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑i : G) • k)) i

Tactic:
ne_of_gt (hρ (i : G) (hms i.2) _ ?_)

Premises used: Set.Mem, setOf, ne_of_gt, Function.support, Subtype.val, Not, 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∞)
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))
i : (↑m : Type u_1)
refine : s ∩ (↑i : G) • k ∈ 𝓝[s] (↑i : G)
⊢ Membership.mem (γ := Set (↑m : Type u_1))
    (support (M := ℝ≥0∞) fun (i : (↑m : Type u_1)) ↦ (ρ : (a : Set G) → ℝ≥0∞) (s ∩ (↑i : G) • k)) i

Tactic:
refine ne_of_gt (hρ (i : G) (hms i.2) _ ?_)

Premises used: ne_of_gt, Subtype.val, 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∞)
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))
i : (↑m : Type u_1)
⊢ (↑i : G) • k ∈ 𝓝 (↑i : G)

Tactic:
simpa
-- 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))
i : (↑m : Type u_1)
⊢ s ∩ (↑i : G) • k ∈ 𝓝[s] (↑i : G)

Tactic:
exact inter_mem_nhdsWithin s (by simpa)

Premises used: inter_mem_nhdsWithin
-- 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:
have : support (fun (i : m) ↦ ρ (s ∩ (i : G) • k)) = univ := by
        refine eq_univ_iff_forall.2 fun i ↦ ?_
        refine ne_of_gt (hρ (i : G) (hms i.2) _ ?_)
        exact inter_mem_nhdsWithin s (by simpa)
-- 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_1 : 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))
this :
  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
⊢ Set.Countable.{u_1} (α := (↑m : Type u_1)) univ

Tactic:
rw [this] at C
-- 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_1 : 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))
this :
  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
C₁ : Set.Countable.{u_1} (α := (↑m : Type u_1)) univ
⊢ 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:
rw [this] at C
-- 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_1 : 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)) univ
this :
  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
⊢ Countable.{u_1 + 1} (↑m : Type u_1)

Tactic:
have : Countable m := countable_univ_iff.mp C
-- 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_1 : 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)) univ
this_2 :
  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
this : Countable.{u_1 + 1} (↑m : Type u_1)
⊢ m.Countable

Tactic:
to_countable m

Premises used: Set.to_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
ρ : 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_1 : 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)) univ
this_2 :
  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
this : Countable.{u_1 + 1} (↑m : Type u_1)
⊢ m.Countable

Tactic:
exact to_countable m

Premises used: Set.to_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
⊢ ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have H : ∀ (ρ : Measure G), IsEverywherePos ρ s → ρ s = ∞ := by
      intro ρ hρ
      have M : ∀ (i : ↑m), MeasurableSet (s ∩ (i : G) • k) :=
        fun i ↦ hs.inter (IsClosed.smul k_closed _).measurableSet
      contrapose! h'm
      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
      have C : Set.Countable (support fun (i : m) ↦ ρ (s ∩ (i : G) • k)) :=
        Summable.countable_support_ennreal this.ne
      have : support (fun (i : m) ↦ ρ (s ∩ (i : G) • k)) = univ := by
        refine eq_univ_iff_forall.2 fun i ↦ ?_
        refine ne_of_gt (hρ (i : G) (hms i.2) _ ?_)
        exact inter_mem_nhdsWithin s (by simpa)
      rw [this] at C
      have : Countable m := countable_univ_iff.mp C
      exact to_countable 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
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ν.IsEverywherePos s

Tactic:
have Hν : IsEverywherePos ν s :=
      h's.smul_measure_nnreal (haarScalarFactor_pos_of_isHaarMeasure _ _).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
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
apply :
  ∀ (x : G) (_hx : x ∈ s),
    ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)
⊢ μ'.IsEverywherePos s

Tactic:
apply Hν.of_forall_exists_nhds_eq (fun x _hx ↦ ?_)

Premises used: MeasureTheory.Measure.IsEverywherePos.of_forall_exists_nhds_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}
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
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
⊢ ∃ (t : Set G), IsCompact t ∧ t ∈ 𝓝 x

Tactic:
exists_compact_mem_nhds x

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- 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
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
obtain :
  ∀ (t : Set G) (t_comp : IsCompact t) (t_mem : t ∈ 𝓝 x),
    ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
obtain ⟨t, t_comp, t_mem⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x := exists_compact_mem_nhds x

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds
-- 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
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
t : Set G
t_comp : IsCompact t
t_mem : t ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
⟨t, t_mem, fun u hu ↦ ?_⟩

Premises used: And.intro, Exists.intro