-- 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
⊢ ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

Tactic:
have int_g_pos : 0 < ∫ x, g x ∂μ :=
  g_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero 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, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

Proof state:
case pos
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 • μ

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:
swap

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
⊢ ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

case pos
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 • μ

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, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

Tactic:
let c : ℝ := (∫ x, g x ∂μ) ⁻¹ * (∫ x, g x ∂μ')

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, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

Proof state:
case neg.inr
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
hf : LocallyCompactSpace G
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂0 • μ

Tactic:
exact (H hf).elim

Result:
no goals

Proof state:
case pos
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:
obtain ⟨⟨g, g_cont⟩, g_comp, g_nonneg, g_one⟩ :
  ∃ (g : C(G, ℝ)), HasCompactSupport g ∧ 0 ≤ g ∧ g 1 ≠ 0 := exists_continuous_nonneg_pos 1

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
⊢ ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ