-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
theorem _root_.MonoidHom.measurePreserving
    {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H]
    [MeasurableSpace H] [BorelSpace H]
    {μ : Measure G} [IsHaarMeasure μ] {ν : Measure H} [IsHaarMeasure ν]
    {f : G →* H} (hcont : Continuous f) (hsurj : Surjective f) (huniv : μ univ = ν univ) :
    MeasurePreserving f μ ν where
  measurable := hcont.measurable
  map_eq

Proof state:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝ : IsFiniteMeasure μ
this : (map (⇑f) μ).IsHaarMeasure
⊢ map (⇑f) μ = ν

Tactic:
set C : ℝ≥0 := haarScalarFactor (μ.map f) ν

Result:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝ : IsFiniteMeasure μ
this : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
⊢ map (⇑f) μ = ν

Proof state:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝ : IsFiniteMeasure μ
this : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
hC : map (⇑f) μ = C • ν
⊢ C = 1

Tactic:
have : C * ν univ = 1 * ν univ := by
  rw [one_mul, ← smul_eq_mul, ← ENNReal.smul_def, ← smul_apply, ← hC,
    map_apply hcont.measurable .univ, preimage_univ, huniv]

Result:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝¹ : IsFiniteMeasure μ
this✝ : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
hC : map (⇑f) μ = C • ν
this : ↑C * ν univ = 1 * ν univ
⊢ C = 1

Proof state:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
⊢ map (⇑f) μ = ν

Tactic:
have : IsFiniteMeasure μ := ⟨by rw [huniv]; apply measure_lt_top⟩

Result:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this : IsFiniteMeasure μ
⊢ map (⇑f) μ = ν