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
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∞)
a₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(measure_mono inter_subset_right).trans (measure_toMeasurable s).le

Premises used: Eq.le, MeasureTheory.measure_toMeasurable, MeasureTheory.measure_mono, LE.le.trans, Set.inter_subset_right
-- 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
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact (measure_mono inter_subset_right).trans (measure_toMeasurable s).le

Premises used: Eq.le, MeasureTheory.measure_toMeasurable, MeasureTheory.measure_mono, LE.le.trans, Set.inter_subset_right
-- 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
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_mono st

Premises used: MeasureTheory.measure_mono
-- 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
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact measure_mono st

Premises used: MeasureTheory.measure_mono
-- 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
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∞)

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
-- 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
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∞)
simp :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞) (↑(μ'.haarScalarFactor μ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [← mu'_t, ← mu_t, nnreal_smul_coe_apply]

Premises used: MeasureTheory.Measure.nnreal_smul_coe_apply
-- 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
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₂ : 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∞)

Tactic:
apply B
-- 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
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∞)
⊢ MeasurableSet t

Tactic:
(measurableSet_toMeasurable _ _).inter (measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasurableSet.inter
-- 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
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∞)
⊢ MeasurableSet t

Tactic:
exact (measurableSet_toMeasurable _ _).inter (measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasurableSet.inter
-- 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
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
mu_t.le.trans_lt hs.lt_top

Premises used: Eq.le, Ne.lt_top, LE.le.trans_lt
-- 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
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact mu_t.le.trans_lt hs.lt_top

Premises used: Eq.le, Ne.lt_top, LE.le.trans_lt
-- 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
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
mu'_t.le.trans_lt h's.lt_top

Premises used: Eq.le, Ne.lt_top, LE.le.trans_lt
-- 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
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact mu'_t.le.trans_lt h's.lt_top

Premises used: Eq.le, Ne.lt_top, LE.le.trans_lt
-- 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
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
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 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hs.measure_eq_iSup_isCompact, hs.measure_eq_iSup_isCompact]

Premises used: MeasurableSet.measure_eq_iSup_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 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
s : Set G
hs : MeasurableSet s
h :
  ∀ (K : Set G) (_Ks : K ⊆ s) (K_comp : IsCompact K),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)

Tactic:
congr! 4 with K _Ks K_comp
-- 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
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
s : Set G
hs : MeasurableSet s
K : Set G
_Ks : K ⊆ s
K_comp : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne
    K_comp.measure_lt_top.ne

Premises used: MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, IsCompact.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
s : Set G
hs : MeasurableSet s
K : Set G
_Ks : K ⊆ s
K_comp : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne
    K_comp.measure_lt_top.ne

Premises used: MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, IsCompact.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
U : Set G
hU : IsOpen[inst] U
rw :
  Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
rw [hU.measure_eq_iSup_isCompact, hU.measure_eq_iSup_isCompact]

Premises used: IsOpen.measure_eq_iSup_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 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
U : Set G
hU : IsOpen[inst] U
h :
  ∀ (K : Set G) (_KU : K ⊆ U) (K_comp : IsCompact K),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)

Tactic:
congr! 4 with K _KU K_comp