awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have μ'₁ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable ν s ∩ closure[inst] s) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable ν s ∩ closure[inst] s) : ℝ≥0∞)
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 _ _ _ _
      · 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : 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∞)
have apply : MeasurableSet (toMeasurable μ' s ∩ closure[inst] s)
Tactic: apply (measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
apply : MeasurableSet (toMeasurable μ' s ∩ closure[inst] s)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
have apply₁ : IsCompact (closure[inst] (toMeasurable μ' s ∩ closure[inst] s))
Tactic: apply (measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ' : (a : Set G) → ℝ≥0∞) s
have ν₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
  ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : CompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsMulLeftInvariant
inst_8 : IsFiniteMeasureOnCompacts μ'
⊢ μ' = μ'.haarScalarFactor μ • μ
have h : ∀ (s : Set G) (_hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s _hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : CompactSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
⊢ μ.InnerRegular
have rw : (HSMul.hSMul (β := Measure G) (μ.haarScalarFactor haar) haar).InnerRegular
Tactic: rw [isMulInvariant_eq_smul_of_compactSpace μ haar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : CompactSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
⊢ μ.Regular
have rw : (HSMul.hSMul (β := Measure G) (μ.haarScalarFactor haar) haar).Regular
Tactic: rw [isMulInvariant_eq_smul_of_compactSpace μ haar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
⊢ CompactSpace G
have by_contra : ∀ (H : ¬CompactSpace G), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
H : ¬CompactSpace G
⊢ False
have H₁ : NoncompactSpace G
Tactic: rw [not_compactSpace_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
⊢ μ' = μ
have this : CompactSpace G
Tactic: have : CompactSpace G := by
    by_contra H
    rw [not_compactSpace_iff] at H
    simpa using measure_univ_of_isMulLeftInvariant μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : IsProbabilityMeasure μ
inst_7 : IsProbabilityMeasure μ'
inst_8 : μ.IsHaarMeasure
inst_9 : μ'.IsHaarMeasure
this : CompactSpace G
⊢ μ' = μ
have A : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : 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∞)
⊢ μ' = μ
have Z : (μ' : (a : Set G) → ℝ≥0∞) univ = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: have Z := A univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : 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∞)
⊢ μ' = μ
have Z₁ : 1 = μ'.haarScalarFactor μ
Tactic: simp only [measure_univ, ENNReal.smul_def, smul_eq_mul, mul_one, ENNReal.one_eq_coe] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : 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 μ
⊢ μ' = μ
have 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have change : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: change μ' s = ν s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ ∃ (k : Set G), IsCompact k ∧ IsClosed[inst] k ∧ Membership.mem (γ := Filter G) (𝓝 1) k
have 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
Tactic: rcases exists_compact_mem_nhds (1 : G) with ⟨k, hk, hmem⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have one_k : 1 ∈ k
Tactic: have one_k : 1 ∈ k := mem_of_mem_nhds k_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
⊢ ∃ (m : Set G), Maximal (fun (x : Set G) ↦ x ∈ A) m
have h : ∀ c ⊆ A, IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c → ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub
Tactic: apply zorn_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
⊢ ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub
have h : ⋃ a ∈ c, a ⊆ s
Tactic: refine ⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
h : ⋃ a ∈ c, a ⊆ s
⊢ ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub
have h₁ : PairwiseDisjoint (α := Set G) (⋃ a ∈ c, a) fun (x : G) ↦ x • k
Tactic: refine ⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
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
⊢ ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub
have h₂ : ∀ s ∈ c, s ⊆ ⋃ a ∈ c, a
Tactic: refine ⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
⊢ ⋃ a ∈ c, a ⊆ s
have h : ∀ (i : Set G) (i_1 : i ∈ c), i ⊆ s
Tactic: simp only [iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
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
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
have hx₁ : ∃ i ∈ c, x ∈ i
Tactic: simp only [mem_iUnion, exists_prop] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
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
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
have hy₁ : ∃ i ∈ c, y ∈ i
Tactic: simp only [mem_iUnion, exists_prop] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
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
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
have h : ∀ (a : Set G) (ac : a ∈ c) (xa : x ∈ a), onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
Tactic: rcases hx with ⟨a, ac, xa⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
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
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
have h : ∀ (b : Set G) (bc : b ∈ c) (yb : y ∈ b), onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
Tactic: rcases hy with ⟨b, bc, yb⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun (x1 x2 : Set G) ↦ x1 ⊆ x2) c
x y : G
hxy : x ≠ y
a : Set G
ac : a ∈ c
xa : x ∈ a
b : Set G
bc : b ∈ c
yb : y ∈ b
⊢ onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
have h : ∀ (m : Set G) (mc : m ∈ c) (am : a ⊆ m) (bm : b ⊆ m), onFun (β := Set G) Disjoint (fun (x : G) ↦ x • k) x y
Tactic: obtain ⟨m, mc, am, bm⟩ : ∃ m ∈ c, a ⊆ m ∧ b ⊆ m := hc.directedOn _ ac _ bc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have obtain : ∀ (m : Set G) (m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: obtain ⟨m, m_max⟩ : ∃ m, Maximal (· ∈ A) m := by
    apply zorn_subset
    intro c cA hc
    refine ⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩
    · simp only [iUnion_subset_iff]
      intro a ac x hx
      simp only [A, subset_def, mem_setOf_eq] at cA
      exact (cA _ ac).1 x hx
    · rintro x hx y hy hxy
      simp only [mem_iUnion, exists_prop] at hx hy
      rcases hx with ⟨a, ac, xa⟩
      rcases hy with ⟨b, bc, yb⟩
      obtain ⟨m, mc, am, bm⟩ : ∃ m ∈ c, a ⊆ m ∧ b ⊆ m := hc.directedOn _ ac _ bc
      exact (cA mc).2 (am xa) (bm yb) hxy
    · intro a ac
      exact subset_biUnion_of_mem (u := id) ac