-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on
compacts and inner regular for finite measure sets with respect to compact sets,
they coincide in the following sense: they give the same value to finite measure sets,
up to a multiplicative constant. -/
@[to_additive]
lemma measure_isMulLeftInvariant_eq_smul_of_ne_top [LocallyCompactSpace G]
    (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ']
    [InnerRegularCompactLTTop μ] [InnerRegularCompactLTTop μ'] {s : Set G}
    (hs : μ s ≠ ∞) (h's : μ' 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
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
this : (c • μ) s ≠ ⊤
⊢ μ' s = (c • μ) s

Tactic:
rw [s_meas.measure_eq_iSup_isCompact_of_ne_top h's.ne,
    s_meas.measure_eq_iSup_isCompact_of_ne_top this]

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
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
this : (c • μ) s ≠ ⊤
⊢ ⨆ K, ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), μ' K = ⨆ K, ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (c • μ) K

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
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
⊢ μ' s = (c • μ) s

Tactic:
have : (c • μ) s ≠ ∞ := by simp [ENNReal.mul_eq_top, hs.ne]

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
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
this : (c • μ) s ≠ ⊤
⊢ μ' s = (c • μ) s

Proof state:
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
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ⊤
h's : μ' s ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : μ' t = μ' s
mu_t : μ t = μ s
⊢ μ t < ⊤

Tactic:
exact mu_t.le.trans_lt hs.lt_top

Result:
no goals

Proof state:
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
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ⊤
h's : μ' s ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : μ' t = μ' s
mu_t : μ t = μ s
⊢ MeasurableSet t

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

Result:
no goals

Proof state:
case h.e'_4.h.f.f
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
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
this : (c • μ) s ≠ ⊤
K : Set G
_Ks : K ⊆ s
K_comp : IsCompact K
⊢ μ' K = (c • μ) K

Tactic:
exact measure_isMulInvariant_eq_smul_of_isCompact_closure μ' μ K_comp.closure

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
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
this : (c • μ) s ≠ ⊤
⊢ ⨆ K, ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), μ' K = ⨆ K, ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (c • μ) K

Tactic:
congr! 4 with K _Ks K_comp

Result:
case h.e'_4.h.f.f
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
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ⊤
h's✝ : μ' s✝ ≠ ⊤
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ⊤
h's : μ' s < ⊤
this : (c • μ) s ≠ ⊤
K : Set G
_Ks : K ⊆ s
K_comp : IsCompact K
⊢ μ' K = (c • μ) K