-- 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
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
⊢ map (⇑f) μ = ν

Tactic:
have hC : μ.map f = C • ν := isMulLeftInvariant_eq_smul_of_innerRegular _ _

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 • ν
⊢ 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 * ν univ = 1 * ν univ

Tactic:
rw [one_mul, ← smul_eq_mul, ← ENNReal.smul_def, ← smul_apply, ← hC,
  map_apply hcont.measurable .univ, preimage_univ, huniv]

Result:
no goals

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 • ν
⊢ map (⇑f) μ = ν

Tactic:
suffices C = 1 by rwa [this, one_smul] at hC

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 • ν
⊢ 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
this : IsFiniteMeasure μ
⊢ map (⇑f) μ = ν

Tactic:
have : (μ.map f).IsHaarMeasure := isHaarMeasure_map_of_isFiniteMeasure μ f hcont hsurj

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
⊢ 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 • ν
this : ↑C * ν univ = 1 * ν univ
⊢ C = 1

Tactic:
rwa [ENNReal.mul_left_inj (NeZero.ne _) (measure_ne_top _ _), ENNReal.coe_eq_one] at this

Result:
no goals

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
⊢ ν univ < ⊤

Tactic:
apply measure_lt_top

Result:
no goals

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 • ν
this : C = 1
⊢ map (⇑f) μ = ν

Tactic:
rwa [this, one_smul] at hC

Result:
no goals

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
⊢ μ univ < ⊤

Tactic:
rw [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
⊢ ν univ < ⊤