-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@[to_additive addHaarScalarFactor_eq_mul]
lemma haarScalarFactor_eq_mul (μ' μ ν : Measure G)
    [IsHaarMeasure μ] [IsHaarMeasure ν] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] :
    haarScalarFactor μ' ν = haarScalarFactor μ' μ * haarScalarFactor μ ν

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : 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
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ 0 < ∫ (x : G), g x ∂ν

Tactic:
apply (integral_pos_iff_support_of_nonneg g_nonneg _).2

Result:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : 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
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ 0 < ν (support ((fun f => f.toFun) { toFun := g, continuous_toFun := g_cont }))

G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : 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
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ Integrable ((fun f => f.toFun) { toFun := g, continuous_toFun := g_cont }) ν

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

Tactic:
by_cases hG : LocallyCompactSpace G

Result:
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✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : ¬LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : 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
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : ¬LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

Tactic:
simp [haarScalarFactor, hG]

Result:
no goals

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✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : 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 ∂ν
Z : ↑(μ'.haarScalarFactor ν) * ∫ (x : G), g x ∂ν = ↑(μ'.haarScalarFactor μ * μ.haarScalarFactor ν) * ∫ (x : G), g x ∂ν
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

Tactic:
simpa only [mul_eq_mul_right_iff (M₀ := ℝ), int_g_pos.ne', or_false, ← NNReal.eq_iff] using 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
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : 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
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ 0 < ν (support ((fun f => f.toFun) { toFun := g, continuous_toFun := g_cont }))

Tactic:
exact IsOpen.measure_pos ν g_cont.isOpen_support ⟨1, g_one⟩

Result:
no goals