G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
⊢ map (fun g => g ^ n) μ = μ
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
⊢ map (fun g => g ^ n) μ = μ
let f := @zpowGroupHom G _ n
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
⊢ map (fun g => g ^ n) μ = μ
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
⊢ map (fun g => g ^ n) μ = μ
have hf : Continuous f := continuous_zpow n
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
⊢ map (fun g => g ^ n) μ = μ
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
⊢ map (fun g => g ^ n) μ = μ
haveI : (μ.map f).IsHaarMeasure :=
  isHaarMeasure_map μ f hf (RootableBy.surjective_pow G ℤ hn) (by simp)
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
⊢ map (fun g => g ^ n) μ = μ
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
⊢ map (fun g => g ^ n) μ = μ
obtain ⟨C, -, -, hC⟩ := isHaarMeasure_eq_smul_isHaarMeasure (μ.map f) μ
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
⊢ C = 1
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
⊢ map (fun g => g ^ n) μ = μ
suffices C = 1 by rwa [this, one_smul] at hC
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
h_univ : ↑↑(map (↑f) μ) univ = ↑↑μ univ
⊢ C = 1
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
⊢ C = 1
have h_univ : (μ.map f) univ = μ univ := by
  rw [map_apply_of_aemeasurable hf.measurable.aemeasurable MeasurableSet.univ,
    preimage_univ]
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
h_univ : ↑↑(map (↑f) μ) univ = ↑↑μ univ
hμ₀ : ↑↑μ univ ≠ 0
⊢ C = 1
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
h_univ : ↑↑(map (↑f) μ) univ = ↑↑μ univ
⊢ C = 1
have hμ₀ : μ univ ≠ 0 := IsOpenPosMeasure.open_pos univ isOpen_univ univ_nonempty
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
h_univ : ↑↑(map (↑f) μ) univ = ↑↑μ univ
hμ₀ : ↑↑μ univ ≠ 0
hμ₁ : ↑↑μ univ ≠ ⊤
⊢ C = 1
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
h_univ : ↑↑(map (↑f) μ) univ = ↑↑μ univ
hμ₀ : ↑↑μ univ ≠ 0
⊢ C = 1
have hμ₁ : μ univ ≠ ∞ := CompactSpace.isFiniteMeasure.measure_univ_lt_top.ne
no goals
case intro.intro.intro
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
h_univ : ↑↑(map (↑f) μ) univ = ↑↑μ univ
hμ₀ : ↑↑μ univ ≠ 0
hμ₁ : ↑↑μ univ ≠ ⊤
⊢ C = 1
rwa [hC, smul_apply, Algebra.id.smul_eq_mul, mul_comm, ← ENNReal.eq_div_iff hμ₀ hμ₁,
  ENNReal.div_self hμ₀ hμ₁] at h_univ
no goals
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
⊢ Filter.Tendsto (↑f) (Filter.cocompact G) (Filter.cocompact G)
simp
no goals
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this✝ : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
this : C = 1
⊢ map (fun g => g ^ n) μ = μ
rwa [this, one_smul] at hC
no goals
G : Type u_1
inst✝⁹ : CommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : T2Space G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : SecondCountableTopology G
μ : Measure G
inst✝² : IsHaarMeasure μ
inst✝¹ : CompactSpace G
inst✝ : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
f : G →* G := zpowGroupHom n
hf : Continuous ↑f
this : IsHaarMeasure (map (↑f) μ)
C : ℝ≥0∞
hC : map (↑f) μ = C • μ
⊢ ↑↑(map (↑f) μ) univ = ↑↑μ univ
rw [map_apply_of_aemeasurable hf.measurable.aemeasurable MeasurableSet.univ,
  preimage_univ]