awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
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∞)
⊢ 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:
conv_rhs => rw [μeq]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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)
      ((HPow.hPow (β := ℕ) c 2 • μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)

Tactic:
have : c ^ 2 * μ K = 1 ^ 2 * μ K := by
    conv_rhs => rw [μeq]
    simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ c = 1

Tactic:
have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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_eq_self₂ inv_eq_self₃ : μ = μ
⊢ μ.inv = μ

Tactic:
rw [hc, this, one_smul]

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
inv_eq_self : μ.inv = μ
⊢ μ.IsInvInvariant

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 = c • μ

Tactic:
have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_innerRegular μ.inv μ
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
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 • μ
rw₆ rw₇ : (c * c) • μ = (c * c) • μ
⊢ map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ

Tactic:
rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]

Premises used: pow_two, smul_smul, MeasureTheory.Measure.map_smul, MeasureTheory.Measure.inv_def
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ

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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
⊢ 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

Premises used: Continuous.measurable, ContinuousInv.continuous_inv, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
this : map ((fun (a : G) ↦ a⁻¹) ∘ fun (a : G) ↦ a⁻¹) μ = HPow.hPow (β := ℕ) c 2 • μ
⊢ μ = HPow.hPow (β := ℕ) c 2 • μ

Tactic:
simpa only [inv_involutive, Involutive.comp_self, Measure.map_id]

Premises used: MeasureTheory.Measure.map_id, inv_involutive, Function.Involutive.comp_self
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
⊢ μ = 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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
inv_eq_self : ∀ (K : PositiveCompacts G), μ.inv = μ
⊢ μ.inv = μ

Tactic:
have K : PositiveCompacts G := Classical.arbitrary _
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
rw :
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2)
    ((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:
rw [μeq]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
this : map Inv.inv (map Inv.inv μ) = HPow.hPow (β := ℕ) c 2 • μ
μeq : μ = HPow.hPow (β := ℕ) c 2 • μ
K : PositiveCompacts G
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∞)
⊢ 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:
conv_rhs => rw [μeq]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
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)
      ((HPow.hPow (β := ℕ) c 2 • μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
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∞)

Tactic:
have : c ^ 2 * μ K = 1 ^ 2 * μ K := by
    conv_rhs => rw [μeq]
    simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
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
⊢ c = 1

Tactic:
have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • μ
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_eq_self₂ inv_eq_self₃ : μ = μ
⊢ μ.inv = μ

Tactic:
rw [hc, this, one_smul]

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : CompactSpace G
inst_7 : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
⊢ MeasurePreserving (fun (g : G) ↦ g ^ n) μ μ

Tactic:
(zpowGroupHom n).measurePreserving (μ := μ) (continuous_zpow n)
    (RootableBy.surjective_pow G ℤ hn) rfl

Premises used: continuous_zpow, Int, MonoidHom.measurePreserving, rfl, RootableBy.surjective_pow
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : CompactSpace G
inst_7 : RootableBy G ℤ
n : ℤ
hn : n ≠ 0
X : Type u_2
inst_8 : MeasurableSpace X
μ' : Measure X
f : X → G
hf : MeasurePreserving f μ' μ
⊢ MeasurePreserving (fun (x : X) ↦ f x ^ n) μ' μ

Tactic:
(measurePreserving_zpow μ hn).comp hf

Premises used: MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.measurePreserving_zpow
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
⊢ ∃ (f : C(A, ℝ)),
    HasCompactSupport (α := A) (β := ℝ) (⇑f : (a : A) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
exists_continuous_nonneg_pos 0

Premises used: exists_continuous_nonneg_pos, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
obtain :
  ∀ (f : A → ℝ) (f_cont : Continuous[inst_4, _] f)
    (f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ))
    (f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) })
    (f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)),
    (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν
⊢ (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν

Tactic:
obtain ⟨⟨f, f_cont⟩, f_comp, f_nonneg, f_zero⟩ :
    ∃ f : C(A, ℝ), HasCompactSupport f ∧ 0 ≤ f ∧ f 0 ≠ 0 := exists_continuous_nonneg_pos 0

Premises used: exists_continuous_nonneg_pos, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0

Tactic:
have int_f_ne_zero : ∫ x, f x ∂g • ν ≠ 0 :=
    (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
a : (↑((g • μ).addHaarScalarFactor (g • ν)) : ℝ) = (↑(μ.addHaarScalarFactor ν) : ℝ)
⊢ (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν

Tactic:
apply NNReal.coe_injective

Premises used: NNReal.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
a :
  HDiv.hDiv (α := ℝ) (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂μ)
      (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂ν) =
    (↑(μ.addHaarScalarFactor ν) : ℝ)
⊢ (↑((g • μ).addHaarScalarFactor (g • ν)) : ℝ) = (↑(μ.addHaarScalarFactor ν) : ℝ)

Tactic:
rw [addHaarScalarFactor_eq_integral_div (g • μ) (g • ν) f_cont f_comp int_f_ne_zero,
    integral_domSMul, integral_domSMul]

Premises used: MeasureTheory.integral_domSMul, MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
⊢ Continuous[inst_4, _] fun (x : A) ↦ f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x)

Tactic:
fun_prop