awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
H : Type u_2
inst_5 : Group H
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalGroup H
inst_8 : CompactSpace H
inst_9 : MeasurableSpace H
inst_10 : BorelSpace H
μ : Measure G
inst_11 : μ.IsHaarMeasure
ν : Measure H
inst_12 : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst, inst_6] (⇑f : (a : G) → H)
hsurj : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
huniv : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure μ
this : IsHaarMeasure.{u_2} (G := H) (map (⇑f : (a : G) → H) μ)
C : ℝ≥0 := haarScalarFactor (map (⇑f : (a : G) → H) μ) ν
hC : map (⇑f : (a : G) → H) μ = C • ν
rw : HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) = (ν : (a : Set H) → ℝ≥0∞) univ
rw₁ : HSMul.hSMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) = (ν : (a : Set H) → ℝ≥0∞) univ
rw₂ : HSMul.hSMul (β := ℝ≥0∞) C ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) = (ν : (a : Set H) → ℝ≥0∞) univ
rw₃ : Eq (α := ℝ≥0∞) ((C • ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
rw₄ :
  Eq (α := ℝ≥0∞) (((map (⇑f : (a : G) → H) μ : Measure H) : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
rw₅ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) univ) : ℝ≥0∞)
    ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
rw₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₇ : Eq (α := ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [one_mul, ← smul_eq_mul, ← ENNReal.smul_def, ← smul_apply, ← hC,
        map_apply hcont.measurable .univ, preimage_univ, huniv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
H : Type u_2
inst_5 : Group H
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalGroup H
inst_8 : CompactSpace H
inst_9 : MeasurableSpace H
inst_10 : BorelSpace H
μ : Measure G
inst_11 : μ.IsHaarMeasure
ν : Measure H
inst_12 : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst, inst_6] (⇑f : (a : G) → H)
hsurj : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
huniv : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure μ
this : IsHaarMeasure.{u_2} (G := H) (map (⇑f : (a : G) → H) μ)
C : ℝ≥0 := haarScalarFactor (map (⇑f : (a : G) → H) μ) ν
hC : map (⇑f : (a : G) → H) μ = C • ν
⊢ C = 1
have this₁ : HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
H : Type u_2
inst_5 : Group H
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalGroup H
inst_8 : CompactSpace H
inst_9 : MeasurableSpace H
inst_10 : BorelSpace H
μ : Measure G
inst_11 : μ.IsHaarMeasure
ν : Measure H
inst_12 : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst, inst_6] (⇑f : (a : G) → H)
hsurj : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
huniv : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure μ
this_2 : IsHaarMeasure.{u_2} (G := H) (map (⇑f : (a : G) → H) μ)
C : ℝ≥0 := haarScalarFactor (map (⇑f : (a : G) → H) μ) ν
hC : map (⇑f : (a : G) → H) μ = C • ν
this :
  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ C = 1
have rwa : ∀ (this : (↑C : ℝ≥0∞) = 1), C = 1
Tactic: rwa [ENNReal.mul_left_inj (NeZero.ne _) (measure_ne_top _ _), ENNReal.coe_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
H : Type u_2
inst_5 : Group H
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalGroup H
inst_8 : CompactSpace H
inst_9 : MeasurableSpace H
inst_10 : BorelSpace H
μ : Measure G
inst_11 : μ.IsHaarMeasure
ν : Measure H
inst_12 : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst, inst_6] (⇑f : (a : G) → H)
hsurj : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
huniv : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure μ
this_2 : IsHaarMeasure.{u_2} (G := H) (map (⇑f : (a : G) → H) μ)
C : ℝ≥0 := haarScalarFactor (map (⇑f : (a : G) → H) μ) ν
hC : map (⇑f : (a : G) → H) μ = C • ν
this :
  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞)
rwa : ∀ (this : (↑C : ℝ≥0∞) = 1), C = 1
⊢ C = 1
have rwa₁ : ∀ (this : C = 1), C = 1
Tactic: rwa [ENNReal.mul_left_inj (NeZero.ne _) (measure_ne_top _ _), ENNReal.coe_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
⊢ μ.IsInvInvariant
have inv_eq_self : μ.inv = μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
⊢ μ.inv = μ
have hc : μ.inv = c • μ
Tactic: have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_regular μ.inv μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₂ : HSMul.hSMul (β := Measure G) c (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₂ : HSMul.hSMul (β := Measure G) c (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₃ : c • μ.inv = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₂ : HSMul.hSMul (β := Measure G) c (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₃ : c • μ.inv = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₄ : c • c • μ = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₂ : HSMul.hSMul (β := Measure G) c (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₃ : c • μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₄ : c • c • μ = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₅ : (c * c) • μ = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₂ : HSMul.hSMul (β := Measure G) c (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
rw₃ : c • μ.inv = HPow.hPow (β := ℕ) c 2 • μ
rw₄ : c • c • μ = HPow.hPow (β := ℕ) c 2 • μ
rw₅ : (c * c) • μ = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₆ : (c * c) • μ = (c * c) • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
⊢ μ.inv = μ
have this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
Tactic: have : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ := by
    rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
⊢ μ = HPow.hPow (β := ℕ) c 2 • μ
have this₁ : map ((fun (a : G) ↦ a⁻¹) ∘ fun (a : G) ↦ a⁻¹) μ = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [map_map continuous_inv.measurable continuous_inv.measurable] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
⊢ μ.inv = μ
have μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
Tactic: have μeq : μ = c ^ 2 • μ := by
    rw [map_map continuous_inv.measurable continuous_inv.measurable] at this
    simpa only [inv_involutive, Involutive.comp_self, Measure.map_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
⊢ μ.inv = μ
have inv_eq_self : ∀ (K : PositiveCompacts G), μ.inv = μ
Tactic: have K : PositiveCompacts G := Classical.arbitrary _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
| HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2)
  ((HPow.hPow (β := ℕ) c 2 • μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
Tactic: rw [μeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
⊢ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
have conv_rhs : HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2)
    ((HPow.hPow (β := ℕ) c 2 • μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
Tactic: conv_rhs => rw [μeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
⊢ μ.inv = μ
have this₁ : HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
Tactic: have : c ^ 2 * μ K = 1 ^ 2 * μ K := by
    conv_rhs => rw [μeq]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this_1 : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
this :
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
⊢ μ.inv = μ
have this₁ : HPow.hPow (β := ℕ) c 2 = HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2
Tactic: have : c ^ 2 = 1 ^ 2 :=
    (ENNReal.mul_left_inj (measure_pos_of_nonempty_interior _ K.interior_nonempty).ne'
          K.isCompact.measure_lt_top.ne).1 this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this_1 : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
this_2 :
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
this : HPow.hPow (β := ℕ) c 2 = HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2
⊢ μ.inv = μ
have this₁ : c = 1
Tactic: have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this_1 : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
this_2 :
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
this_3 : HPow.hPow (β := ℕ) c 2 = HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2
this : c = 1
⊢ μ.inv = μ
have inv_eq_self : c • μ = μ
Tactic: rw [hc, this, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this_1 : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
this_2 :
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
this_3 : HPow.hPow (β := ℕ) c 2 = HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2
this : c = 1
inv_eq_self : c • μ = μ
⊢ μ.inv = μ
have inv_eq_self₁ : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
Tactic: rw [hc, this, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
this_1 : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
this_2 :
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) c 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
this_3 : HPow.hPow (β := ℕ) c 2 = HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2
this : c = 1
inv_eq_self : c • μ = μ
inv_eq_self₁ : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
⊢ μ.inv = μ
have inv_eq_self₂ : μ = μ
Tactic: rw [hc, this, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.InnerRegular
⊢ μ.IsInvInvariant
have inv_eq_self : μ.inv = μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.InnerRegular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
⊢ μ.inv = μ
have hc : μ.inv = c • μ
Tactic: have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_innerRegular μ.inv μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.InnerRegular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.InnerRegular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
hc : μ.inv = c • μ
rw : map Inv.inv μ.inv = HPow.hPow (β := ℕ) c 2 • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
have rw₁ : map Inv.inv (c • μ) = HPow.hPow (β := ℕ) c 2 • μ
Tactic: rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]