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
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 :
  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:
t_comp.measure_lt_top.ne

Premises used: 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 : μ.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 :
  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:
exact t_comp.measure_lt_top.ne

Premises used: 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 : μ.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 :
  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:
((measure_mono st).trans_lt t_comp.measure_lt_top).ne

Premises used: IsCompact.measure_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, 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 : μ.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 :
  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:
exact ((measure_mono st).trans_lt t_comp.measure_lt_top).ne

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

Tactic:
((measure_mono st).trans_lt t_comp.measure_lt_top).ne

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

Tactic:
exact ((measure_mono st).trans_lt t_comp.measure_lt_top).ne

Premises used: IsCompact.measure_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, 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
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∞)

Tactic:
have A : μ' s = haarScalarFactor μ' ν • ν s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ' ν hs h's
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
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∞)

Tactic:
have B : μ s = haarScalarFactor μ ν • ν s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ ν hs h's
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
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∞)
rw₃ rw₄ :
  HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ * μ.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∞)

Tactic:
rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]

Premises used: smul_smul, MeasureTheory.Measure.haarScalarFactor_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
a : (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
a₁ : HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ' : (a : Set G) → ℝ≥0∞) s
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable ν s ∩ closure[inst] s) : ℝ≥0∞)

Tactic:
measure_mono <| subset_inter (subset_toMeasurable ν s) subset_closure

Premises used: subset_closure, MeasureTheory.subset_toMeasurable, Set.subset_inter, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
apply : MeasurableSet (toMeasurable ν s ∩ closure[inst] s)
apply₁ : IsCompact (closure[inst] (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∞)

Tactic:
apply measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _

Premises used: MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable ν s ∩ closure[inst] s)

Tactic:
(measurableSet_toMeasurable ν s).inter isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.measurableSet_toMeasurable, isClosed_closure, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable ν s ∩ closure[inst] s)

Tactic:
exact (measurableSet_toMeasurable ν s).inter isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.measurableSet_toMeasurable, isClosed_closure, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure[inst] (toMeasurable ν s ∩ closure[inst] s))

Tactic:
h's.closure_of_subset inter_subset_right

Premises used: IsCompact.closure_of_subset, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure[inst] (toMeasurable ν s ∩ closure[inst] s))

Tactic:
exact h's.closure_of_subset inter_subset_right

Premises used: IsCompact.closure_of_subset, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable ν s ∩ closure[inst] s) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable ν s) : ℝ≥0∞)

Tactic:
measure_mono inter_subset_left

Premises used: Set.inter_subset_left, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable ν s) : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_toMeasurable s

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
μ'₁ :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable ν s ∩ closure[inst] s) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable ν s ∩ closure[inst] s) : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) 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

Premises used: subset_closure, Set.inter_subset_left, MeasureTheory.subset_toMeasurable, Inter.inter, MeasureTheory.measure_toMeasurable, Set.subset_inter, closure, MeasureTheory.measure_mono, MeasureTheory.toMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : 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 μ • μ
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)

Tactic:
measure_mono <| subset_inter (subset_toMeasurable μ' s) subset_closure

Premises used: subset_closure, MeasureTheory.subset_toMeasurable, Set.subset_inter, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
apply : MeasurableSet (toMeasurable μ' s ∩ closure[inst] s)
apply₁ : IsCompact (closure[inst] (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∞)

Tactic:
apply (measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _).symm

Premises used: MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable μ' s ∩ closure[inst] s)

Tactic:
(measurableSet_toMeasurable μ' s).inter isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.measurableSet_toMeasurable, isClosed_closure, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable μ' s ∩ closure[inst] s)

Tactic:
exact (measurableSet_toMeasurable μ' s).inter isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.measurableSet_toMeasurable, isClosed_closure, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure[inst] (toMeasurable μ' s ∩ closure[inst] s))

Tactic:
h's.closure_of_subset inter_subset_right

Premises used: IsCompact.closure_of_subset, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure[inst] (toMeasurable μ' s ∩ closure[inst] s))

Tactic:
exact h's.closure_of_subset inter_subset_right

Premises used: IsCompact.closure_of_subset, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s ∩ closure[inst] s) : ℝ≥0∞)
    ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s) : ℝ≥0∞)

Tactic:
measure_mono inter_subset_left

Premises used: Set.inter_subset_left, 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
s : Set G
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (toMeasurable μ' s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_toMeasurable s

Premises used: MeasureTheory.measure_toMeasurable