-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@[to_additive (attr := simp) addHaarScalarFactor_smul]
lemma haarScalarFactor_smul [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
    [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {c : ℝ≥0} :
    haarScalarFactor (c • μ') μ = c • 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✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
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_ne_zero : ∫ (x : G), g x ∂μ ≠ 0
⊢ (∫ (x : G), g x ∂c • μ') / ∫ (x : G), g x ∂μ = (c • ∫ (x : G), g x ∂μ') / ∫ (x : G), g x ∂μ

Tactic:
simp

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
c : ℝ≥0
⊢ (c • μ').haarScalarFactor μ = c • μ'.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 intro.mk.intro.intro
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
c : ℝ≥0
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 • μ').haarScalarFactor μ = c • μ'.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✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
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_ne_zero : ∫ (x : G), g x ∂μ ≠ 0
⊢ c • ((∫ (x : G), g x ∂μ') / ∫ (x : G), g x ∂μ) = c • ↑(μ'.haarScalarFactor μ)

Tactic:
rw [← haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero]

Result:
no goals

Proof state:
case intro.mk.intro.intro.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
c : ℝ≥0
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_ne_zero : ∫ (x : G), g x ∂μ ≠ 0
⊢ ↑((c • μ').haarScalarFactor μ) = ↑(c • μ'.haarScalarFactor μ)

Tactic:
calc
  haarScalarFactor (c • μ') μ = (∫ x, g x ∂(c • μ')) / ∫ x, g x ∂μ :=
    haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero
  _ = (c • (∫ x, g x ∂μ')) / ∫ x, g x ∂μ := by simp
  _ = c • ((∫ x, g x ∂μ') / ∫ x, g x ∂μ) := smul_div_assoc c _ _
  _ = c • haarScalarFactor μ' μ := by
    rw [← haarScalarFactor_eq_integral_div _ _ g_cont g_comp int_g_ne_zero]

Result:
no goals

Proof state:
case intro.mk.intro.intro
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
c : ℝ≥0
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 • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ

Tactic:
have int_g_ne_zero : ∫ x, g x ∂μ ≠ 0 :=
  ne_of_gt (g_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero g_comp g_nonneg g_one)

Result:
case intro.mk.intro.intro
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
c : ℝ≥0
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_ne_zero : ∫ (x : G), g x ∂μ ≠ 0
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ

Proof state:
case intro.mk.intro.intro
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
c : ℝ≥0
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_ne_zero : ∫ (x : G), g x ∂μ ≠ 0
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ

Tactic:
apply NNReal.coe_injective

Result:
case intro.mk.intro.intro.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
c : ℝ≥0
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_ne_zero : ∫ (x : G), g x ∂μ ≠ 0
⊢ ↑((c • μ').haarScalarFactor μ) = ↑(c • μ'.haarScalarFactor μ)