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 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
ν₁ :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ' : (a : Set G) → ℝ≥0∞) s

Tactic:
calc
    ν s ≤ ν ((toMeasurable μ' s) ∩ (closure s)) :=
      measure_mono <| subset_inter (subset_toMeasurable μ' s) subset_closure
    _ = μ' ((toMeasurable μ' s) ∩ (closure s)) := by
      apply (measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _).symm
      · exact (measurableSet_toMeasurable μ' s).inter isClosed_closure.measurableSet
      · exact h's.closure_of_subset inter_subset_right
    _ ≤ μ' (toMeasurable μ' s) := measure_mono inter_subset_left
    _ = μ' s := measure_toMeasurable s

Premises used: subset_closure, Set.inter_subset_left, MeasureTheory.subset_toMeasurable, Inter.inter, MeasureTheory.measure_toMeasurable, Set.subset_inter, closure, MeasureTheory.measure_mono, MeasureTheory.toMeasurable, DFunLike.coe
-- 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 : CompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsMulLeftInvariant
inst_8 : IsFiniteMeasureOnCompacts μ'
h :
  ∀ (s : Set G) (_hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ' = μ'.haarScalarFactor μ • μ

Tactic:
ext s _hs
-- 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 : CompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsMulLeftInvariant
inst_8 : IsFiniteMeasureOnCompacts μ'
s : Set G
_hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact

Premises used: MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure, IsClosed.isCompact, isClosed_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 : CompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsMulLeftInvariant
inst_8 : IsFiniteMeasureOnCompacts μ'
s : Set G
_hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact

Premises used: MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure, IsClosed.isCompact, isClosed_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 : CompactSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
rw : (HSMul.hSMul (β := Measure G) (μ.haarScalarFactor haar) haar).InnerRegular
⊢ μ.InnerRegular

Tactic:
rw [isMulInvariant_eq_smul_of_compactSpace μ haar]

Premises used: MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace, MeasureTheory.Measure.haar
-- 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 : CompactSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
⊢ (HSMul.hSMul (β := Measure G) (μ.haarScalarFactor haar) haar).InnerRegular

Tactic:
infer_instance
-- 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 : CompactSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
rw : (HSMul.hSMul (β := Measure G) (μ.haarScalarFactor haar) haar).Regular
⊢ μ.Regular

Tactic:
rw [isMulInvariant_eq_smul_of_compactSpace μ haar]

Premises used: MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace, MeasureTheory.Measure.haar
-- 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 : CompactSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
⊢ (HSMul.hSMul (β := Measure G) (μ.haarScalarFactor haar) haar).Regular

Tactic:
infer_instance
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
by_contra : ∀ (H : ¬CompactSpace G), False
⊢ CompactSpace G

Tactic:
by_contra H
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
H : ¬CompactSpace G
⊢ NoncompactSpace G

Tactic:
rw [not_compactSpace_iff] at H

Premises used: not_compactSpace_iff
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
H : NoncompactSpace G
⊢ False

Tactic:
simpa using measure_univ_of_isMulLeftInvariant μ

Premises used: MeasureTheory.measure_univ_of_isMulLeftInvariant
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
⊢ CompactSpace G

Tactic:
have : CompactSpace G := by
    by_contra H
    rw [not_compactSpace_iff] at H
    simpa using measure_univ_of_isMulLeftInvariant μ
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
this : CompactSpace G
⊢ ∀ (s : Set G),
    (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have A s : μ' s = haarScalarFactor μ' μ • μ s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
this : CompactSpace G
A :
  ∀ (s : Set G),
    (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) univ =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
have Z := A univ
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
this : CompactSpace G
A :
  ∀ (s : Set G),
    (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Z :
  (μ' : (a : Set G) → ℝ≥0∞) univ =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ 1 = μ'.haarScalarFactor μ

Tactic:
simp only [measure_univ, ENNReal.smul_def, smul_eq_mul, mul_one, ENNReal.one_eq_coe] at Z

Premises used: ENNReal.smul_def, MeasureTheory.IsProbabilityMeasure.measure_univ, ENNReal.one_eq_coe, smul_eq_mul, mul_one
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
this : CompactSpace G
A :
  ∀ (s : Set G),
    (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Z : 1 = μ'.haarScalarFactor μ
h :
  ∀ (s : Set G) (_hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ' = μ

Tactic:
ext s _hs
-- 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 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
this : CompactSpace G
A :
  ∀ (s : Set G),
    (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Z : 1 = μ'.haarScalarFactor μ
s : Set G
_hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [A s, ← Z]
-- 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 μ • μ
change : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
change μ' s = ν s

Premises used: DFunLike.coe
-- 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 μ • μ
rcases :
  ∀ (k : Set G) (hk : IsCompact k) (hmem : Membership.mem (γ := Filter G) (𝓝 1) k),
    ∃ (k : Set G), IsCompact k ∧ IsClosed[inst] k ∧ Membership.mem (γ := Filter G) (𝓝 1) k
⊢ ∃ (k : Set G), IsCompact k ∧ IsClosed[inst] k ∧ Membership.mem (γ := Filter G) (𝓝 1) k

Tactic:
rcases exists_compact_mem_nhds (1 : G) with ⟨k, hk, hmem⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, OfNat.ofNat
-- 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
hk : IsCompact k
hmem : Membership.mem (γ := Filter G) (𝓝 1) k
⊢ ∃ (k : Set G), IsCompact k ∧ IsClosed[inst] k ∧ Membership.mem (γ := Filter G) (𝓝 1) k

Tactic:
⟨closure k, hk.closure, isClosed_closure, mem_of_superset hmem subset_closure⟩

Premises used: subset_closure, IsCompact.closure, closure, And.intro, Exists.intro, isClosed_closure, Filter.mem_of_superset
-- 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
hk : IsCompact k
hmem : Membership.mem (γ := Filter G) (𝓝 1) k
⊢ ∃ (k : Set G), IsCompact k ∧ IsClosed[inst] k ∧ Membership.mem (γ := Filter G) (𝓝 1) k

Tactic:
exact ⟨closure k, hk.closure, isClosed_closure, mem_of_superset hmem subset_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 μ • μ
obtain :
  ∀ (k : Set G) (k_comp : IsCompact k) (k_closed : IsClosed[inst] k) (k_mem : Membership.mem (γ := Filter G) (𝓝 1) k),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
obtain ⟨k, k_comp, k_closed, k_mem⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ k ∈ 𝓝 (1 : G) := by
    rcases exists_compact_mem_nhds (1 : G) with ⟨k, hk, hmem⟩
    exact ⟨closure k, hk.closure, isClosed_closure, mem_of_superset hmem subset_closure⟩

Premises used: nhds, OfNat.ofNat
-- 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
⊢ 1 ∈ k

Tactic:
have one_k : 1 ∈ k := mem_of_mem_nhds k_mem
-- 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}
h : ∀ c ⊆ A, IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c → ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub
⊢ ∃ (m : Set G), Maximal (fun (x : Set G) ↦ x ∈ A) m

Tactic:
apply zorn_subset

Premises used: zorn_subset
-- 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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
⊢ ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub

Tactic:
⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩

Premises used: And.intro, Exists.intro, Set.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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
h : ⋃ a ∈ c, a ⊆ s
h₁ : PairwiseDisjoint (α := Set G) (⋃ a ∈ c, a) fun (x : G) ↦ x • k
h₂ : ∀ s ∈ c, s ⊆ ⋃ a ∈ c, a
⊢ ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub

Tactic:
refine ⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩
-- 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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
h : ∀ (i : Set G) (i_1 : i ∈ c), i ⊆ s
⊢ ⋃ a ∈ c, a ⊆ s

Tactic:
simp only [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- 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}
c : Set (Set G)
cA : ∀ x ∈ c, (∀ x_1 ∈ x, x_1 ∈ s) ∧ x.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
a : Set G
ac : a ∈ c
x : G
hx : x ∈ a
⊢ x ∈ s

Tactic:
(cA _ ac).1 x hx

Premises used: And.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}
c : Set (Set G)
cA : ∀ x ∈ c, (∀ x_1 ∈ x, x_1 ∈ s) ∧ x.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
a : Set G
ac : a ∈ c
x : G
hx : x ∈ a
⊢ x ∈ s

Tactic:
exact (cA _ ac).1 x hx

Premises used: And.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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
x : G
hx : Membership.mem (γ := Set G) (⋃ a ∈ c, a) x
y : G
hy : Membership.mem (γ := Set G) (⋃ a ∈ c, a) y
hxy : x ≠ y
⊢ ∃ i ∈ c, x ∈ i

Tactic:
simp only [mem_iUnion, exists_prop] at hx hy

Premises used: Set.mem_iUnion, exists_prop
-- 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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
x : G
hx : Membership.mem (γ := Set G) (⋃ a ∈ c, a) x
y : G
hy : Membership.mem (γ := Set G) (⋃ a ∈ c, a) y
hxy : x ≠ y
hx₁ : ∃ i ∈ c, x ∈ i
⊢ ∃ i ∈ c, y ∈ i

Tactic:
simp only [mem_iUnion, exists_prop] at hx hy

Premises used: Set.mem_iUnion, exists_prop
-- 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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
x y : G
hxy : x ≠ y
hx : ∃ i ∈ c, x ∈ i
hy : ∃ i ∈ c, y ∈ i
h : ∀ (a : Set G) (ac : a ∈ c) (xa : x ∈ a), onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y

Tactic:
rcases hx with ⟨a, ac, xa⟩
-- 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}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
x y : G
hxy : x ≠ y
hy : ∃ i ∈ c, y ∈ i
a : Set G
ac : a ∈ c
xa : x ∈ a
h : ∀ (b : Set G) (bc : b ∈ c) (yb : y ∈ b), onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y

Tactic:
rcases hy with ⟨b, bc, yb⟩