-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- **Uniqueness of Haar measures**:
Two Haar measures which are probability measures coincide. -/
@[to_additive]
lemma isHaarMeasure_eq_of_isProbabilityMeasure [LocallyCompactSpace G] (μ' μ : Measure G)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [IsHaarMeasure μ] [IsHaarMeasure μ'] :
    μ' = μ

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
⊢ μ' = μ

Tactic:
have A s : μ' s = haarScalarFactor μ' μ • μ s :=
  measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
⊢ μ' = μ

Proof state:
case 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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
Z : 1 = μ'.haarScalarFactor μ
s : Set G
_hs : MeasurableSet s
⊢ μ' s = μ s

Tactic:
simp [A s, ← Z]

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
H : ¬CompactSpace G
⊢ False

Tactic:
rw [not_compactSpace_iff] at H

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
H : NoncompactSpace G
⊢ False

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
Z : 1 = μ'.haarScalarFactor μ
⊢ μ' = μ

Tactic:
ext s _hs

Result:
case 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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
Z : 1 = μ'.haarScalarFactor μ
s : Set G
_hs : MeasurableSet 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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
Z : μ' univ = μ'.haarScalarFactor μ • μ univ
⊢ μ' = μ

Tactic:
simp only [measure_univ, ENNReal.smul_def, smul_eq_mul, mul_one, ENNReal.one_eq_coe] at Z

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
Z : 1 = μ'.haarScalarFactor μ
⊢ μ' = μ

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
⊢ CompactSpace G

Tactic:
by_contra H

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
H : ¬CompactSpace G
⊢ False

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
⊢ μ' = μ

Tactic:
have Z := A univ

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
Z : μ' univ = μ'.haarScalarFactor μ • μ univ
⊢ μ' = μ

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
⊢ μ' = μ

Tactic:
have : CompactSpace G := by
  by_contra H
  rw [not_compactSpace_iff] at H
  simpa using measure_univ_of_isMulLeftInvariant μ

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
⊢ μ' = μ

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
H : NoncompactSpace G
⊢ False

Tactic:
simpa using measure_univ_of_isMulLeftInvariant μ

Result:
no goals