-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- Given two left-invariant measures which are finite on
compacts, they coincide in the following sense: they give the same value to the integral of
continuous compactly supported functions, up to a multiplicative constant. -/
@[to_additive exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport]
lemma exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport (μ' μ : Measure G)
    [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] :
    ∃ (c : ℝ≥0), ∀ (f : G → ℝ), Continuous f → HasCompactSupport f →
      ∫ x, f x ∂μ' = ∫ x, f x ∂(c • μ)

Proof state:
case pos.intro.mk.intro.intro
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ

Tactic:
have B : ∫ x, f x ∂μ' = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ' :=
  integral_isMulLeftInvariant_isMulRightInvariant_combo f_cont f_comp g_cont g_comp g_nonneg g_one

Result:
case pos.intro.mk.intro.intro
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
B : ∫ (x : G), f x ∂μ' = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ'
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ

Proof state:
case pos.intro.mk.intro.intro
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
B : ∫ (x : G), f x ∂μ' = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ'
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ

Tactic:
rw [← A, mul_assoc, mul_comm] at B

Result:
case pos.intro.mk.intro.intro
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
B : ∫ (x : G), f x ∂μ' = ((∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ') * ∫ (x : G), f x ∂μ
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ

Proof state:
case pos.intro.mk.intro.intro
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ

Tactic:
have A : ∫ x, f x ∂μ = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ :=
  integral_isMulLeftInvariant_isMulRightInvariant_combo f_cont f_comp g_cont g_comp g_nonneg g_one

Result:
case pos.intro.mk.intro.intro
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ

Proof state:
case neg
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
⊢ ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

Tactic:
refine ⟨0, fun f f_cont f_comp ↦ ?_⟩

Result:
case neg
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂0 • μ