-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
theorem measure_isMulInvariant_eq_smul_of_isCompact_closure [LocallyCompactSpace G]
    (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ']
    {s : Set G} (h's : IsCompact (closure s)) :
    μ' s = haarScalarFactor μ' μ • μ 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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ μ' s = μ'.haarScalarFactor μ • μ s

Tactic:
apply le_antisymm

Result:
case a
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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ μ' s ≤ μ'.haarScalarFactor μ • μ s

case a
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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ μ'.haarScalarFactor μ • μ 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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure (toMeasurable ν s ∩ closure s))

Tactic:
exact h's.closure_of_subset inter_subset_right

Result:
no goals

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

Tactic:
apply measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _

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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable ν s ∩ closure s)

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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure (toMeasurable ν s ∩ closure 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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable μ' s ∩ closure s)

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

Result:
no goals

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

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

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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable μ' s ∩ closure s)

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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ IsCompact (closure (toMeasurable μ' s ∩ closure 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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ MeasurableSet (toMeasurable ν s ∩ closure s)

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

Result:
no goals

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

Tactic:
exact h's.closure_of_subset inter_subset_right

Result:
no goals

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
s : Set G
h's : IsCompact (closure s)
⊢ μ' s = μ'.haarScalarFactor μ • μ s

Tactic:
let ν := haarScalarFactor μ' μ • μ

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
s : Set G
h's : IsCompact (closure s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ μ' s = μ'.haarScalarFactor μ • μ s