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 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have st : s ⊆ t
Tactic: have st : s ⊆ t := (IsClosed.closure_subset_iff t_closed).mp hf
-- 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
have apply : IsCompact (closure[inst] (t \ s))
Tactic: apply smul_measure_isMulInvariant_le_of_isCompact_closure _ _ (t_closed.measurableSet.diff hs)
-- 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
Tactic: have A : ν (t \ s) ≤ μ' (t \ s) := by
    apply smul_measure_isMulInvariant_le_of_isCompact_closure _ _ (t_closed.measurableSet.diff hs)
    exact t_comp.closure_of_subset diff_subset
-- 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have B : μ' t = ν t :=
    measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_comp
-- 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∀
  (A :
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
  (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rwa [measure_diff st hs.nullMeasurableSet, measure_diff st hs.nullMeasurableSet, ← B,
    ENNReal.sub_le_sub_iff_left] at A
Cleared hypotheses: A, 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h' : ∀
  (A :
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
  (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [measure_diff st hs.nullMeasurableSet, measure_diff st hs.nullMeasurableSet, ← B,
    ENNReal.sub_le_sub_iff_left] at A
Cleared hypotheses: A, 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h' :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rwa : ∀
  (A :
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
      (μ' : (a : Set G) → ℝ≥0∞) (t \ s))
  (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [measure_diff st hs.nullMeasurableSet, measure_diff st hs.nullMeasurableSet, ← B,
    ENNReal.sub_le_sub_iff_left] at A
Cleared hypotheses: A, 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h' :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        (μ' : (a : Set G) → ℝ≥0∞) (t \ s))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rwa₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [measure_diff st hs.nullMeasurableSet, measure_diff st hs.nullMeasurableSet, ← B,
    ENNReal.sub_le_sub_iff_left] at A
-- 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := haar
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have A : (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have A : μ' s = haarScalarFactor μ' ν • ν s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ' ν hs h's
-- 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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := haar
A : (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have B : (μ : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have B : μ s = haarScalarFactor μ ν • ν s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ ν hs h'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
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := haar
A : (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
B : (μ : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]
-- 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
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := haar
A : (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
B : (μ : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
  μ'.haarScalarFactor μ • HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]
-- 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
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := haar
A : (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
B : (μ : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    μ'.haarScalarFactor μ • HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]
-- 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
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := haar
A : (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
B : (μ : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    μ'.haarScalarFactor μ • HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rw₃ : HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]
-- 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 a : (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
a : (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ' : (a : Set G) → ℝ≥0∞) s
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
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 _ _ _ _
-- 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 _ _ _ _