-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- If an invariant measure is inner regular, then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `haarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure, and removes the inner regularity assumption. -/
@[to_additive measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop
" If an invariant measure is inner regular, then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `addHaarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure, and removes the inner regularity assumption."]
lemma measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop
    [LocallyCompactSpace G]
    (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ']
    [InnerRegularCompactLTTop μ]
    {s : Set G} (hs : MeasurableSet s) (h's : IsCompact (closure s)) :
    μ' s = haarScalarFactor μ' μ • μ s

Proof state:
case intro.mk.intro.intro.intro
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
st : s ⊆ t
⊢ μ' s ≤ ν s

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

Result:
case intro.mk.intro.intro.intro
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
st : s ⊆ t
A : ν (t \ s) ≤ μ' (t \ s)
⊢ μ' s ≤ ν s

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
st : s ⊆ t
⊢ ν (t \ s) ≤ μ' (t \ s)

Tactic:
apply smul_measure_isMulInvariant_le_of_isCompact_closure _ _ (t_closed.measurableSet.diff hs)

Result:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
st : s ⊆ t
⊢ IsCompact (closure (t \ s))

Proof state:
case intro.mk.intro.intro.intro
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
⊢ μ' s ≤ ν s

Tactic:
have st : s ⊆ t := (IsClosed.closure_subset_iff t_closed).mp hf

Result:
case intro.mk.intro.intro.intro
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
st : s ⊆ t
⊢ μ' s ≤ ν s

Proof state:
case intro.mk.intro.intro.intro.h
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed t
t_comp : IsCompact t
st : s ⊆ t
A : μ' t - ν s ≤ μ' t - μ' s
B : μ' t = ν t
⊢ μ' s ≤ μ' t

Tactic:
exact measure_mono st

Result:
no goals