awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
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
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have Hμ' : μ'.IsEverywherePos s
Tactic: have Hμ' : IsEverywherePos μ' s := by
      apply Hν.of_forall_exists_nhds_eq (fun x _hx ↦ ?_)
      obtain ⟨t, t_comp, t_mem⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x := exists_compact_mem_nhds x
      refine ⟨t, t_mem, fun u hu ↦ ?_⟩
      apply measure_isMulInvariant_eq_smul_of_isCompact_closure
      exact t_comp.closure_of_subset hu
-- 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
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
Hμ' : μ'.IsEverywherePos s
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [H ν Hν, H μ' Hμ']
-- 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
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
Hμ' : μ'.IsEverywherePos s
neg : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have neg₁ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [H ν Hν, H μ' 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 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have : (c • μ) s ≠ ∞ := by simp [ENNReal.mul_eq_top, hs.ne]
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
  (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (c • μ : (a : Set G) → ℝ≥0∞) K)
Tactic: rw [s_meas.measure_eq_iSup_isCompact_of_ne_top h's.ne,
        s_meas.measure_eq_iSup_isCompact_of_ne_top this]
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (c • μ : (a : Set G) → ℝ≥0∞) K)
have h : ∀ (K : Set G) (_Ks : K ⊆ s) (K_comp : IsCompact K),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: congr! 4 with K _Ks K_comp
-- 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 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have B : ∀ (s : Set G),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have B : ∀ s, MeasurableSet s → μ s < ∞ → μ' s < ∞ → μ' s = (c • μ) s := by
    intro s s_meas hs h's
    have : (c • μ) s ≠ ∞ := by simp [ENNReal.mul_eq_top, hs.ne]
    rw [s_meas.measure_eq_iSup_isCompact_of_ne_top h's.ne,
        s_meas.measure_eq_iSup_isCompact_of_ne_top this]
    congr! 4 with K _Ks K_comp
    exact measure_isMulInvariant_eq_smul_of_isCompact_closure μ' μ K_comp.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 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have st : s ⊆ t
Tactic: have st : s ⊆ t := subset_inter (subset_toMeasurable μ' s) (subset_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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
a : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: apply le_antisymm
-- 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 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have mu'_t : μ' t = μ' s := by
    apply le_antisymm
    · exact (measure_mono inter_subset_left).trans (measure_toMeasurable s).le
    · exact measure_mono st
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
a : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: apply le_antisymm
-- 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 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have mu_t : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have mu_t : μ t = μ s := by
    apply le_antisymm
    · exact (measure_mono inter_subset_right).trans (measure_toMeasurable s).le
    · exact measure_mono st
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
mu_t : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have simp : (μ' : (a : Set G) → ℝ≥0∞) t =
  HMul.hMul (β := ℝ≥0∞) (↑(μ'.haarScalarFactor μ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp only [← mu'_t, ← mu_t, nnreal_smul_coe_apply]
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
mu_t : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞) (↑(μ'.haarScalarFactor μ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have a : MeasurableSet t
Tactic: apply B
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
mu_t : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
a : MeasurableSet t
⊢ (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞) (↑(μ'.haarScalarFactor μ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have a₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply B
-- 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
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
mu_t : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
a : MeasurableSet t
a₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞) (↑(μ'.haarScalarFactor μ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have a₂ : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply B
-- 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
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
⊢ μ' = μ'.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