awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
U : Set G
hU : IsOpen[inst] U
K : Set G
_KU : K ⊆ U
K_comp : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne
      K_comp.measure_lt_top.ne

Premises used: MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, IsCompact.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
U : Set G
hU : IsOpen[inst] U
K : Set G
_KU : K ⊆ U
K_comp : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne
      K_comp.measure_lt_top.ne

Premises used: MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, IsCompact.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
⊢ ∀ (U : Set G),
    IsOpen[inst] U →
      Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
have A : ∀ U, IsOpen U → μ' U = (haarScalarFactor μ' μ • μ) U := by
    intro U hU
    rw [hU.measure_eq_iSup_isCompact, hU.measure_eq_iSup_isCompact]
    congr! 4 with K _KU K_comp
    exact measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne
      K_comp.measure_lt_top.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
A :
  ∀ (U : Set G),
    IsOpen[inst] U →
      Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞)
⊢ μ' = μ'.haarScalarFactor μ • μ

Tactic:
OuterRegular.ext_isOpen A

Premises used: MeasureTheory.Measure.OuterRegular.ext_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
A :
  ∀ (U : Set G),
    IsOpen[inst] U →
      Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞)
⊢ μ' = μ'.haarScalarFactor μ • μ

Tactic:
exact OuterRegular.ext_isOpen A

Premises used: MeasureTheory.Measure.OuterRegular.ext_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ' μ : Measure G
inst_7 : μ.IsHaarMeasure
inst_8 : IsFiniteMeasureOnCompacts μ'
inst_9 : μ'.IsMulLeftInvariant
⊢ μ' = μ'.haarScalarFactor μ • μ

Tactic:
isMulLeftInvariant_eq_smul_of_regular μ' μ

Premises used: MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
have : ∀ (K : PositiveCompacts G), μ ≪ ν
⊢ μ ≪ ν

Tactic:
have K : PositiveCompacts G := Classical.arbitrary _
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
K : PositiveCompacts G
⊢ haarMeasure K = (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) • ν

Tactic:
have h : haarMeasure K = (haarScalarFactor (haarMeasure K) ν : ℝ≥0∞) • ν :=
    isMulLeftInvariant_eq_smul (haarMeasure K) ν
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) • ν
rw :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) •
      ν ≪
    ν
⊢ μ ≪ ν

Tactic:
rw [haarMeasure_unique μ K, h, smul_smul]

Premises used: MeasureTheory.Measure.haarMeasure_unique, smul_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) • ν
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) •
      ν ≪
    ν

Tactic:
smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) • ν
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) •
      ν ≪
    ν

Tactic:
exact smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
rw : LT.lt (α := ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [huniv]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply measure_lt_top

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
⊢ IsFiniteMeasure μ

Tactic:
have : IsFiniteMeasure μ := ⟨by rw [huniv]; apply measure_lt_top⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : IsFiniteMeasure μ
⊢ IsHaarMeasure.{u_2} (G := H) (map (⇑f : (a : G) → H) μ)

Tactic:
have : (μ.map f).IsHaarMeasure := isHaarMeasure_map_of_isFiniteMeasure μ f hcont hsurj
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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) μ) ν
⊢ map (⇑f : (a : G) → H) μ = C • ν

Tactic:
have hC : μ.map f = C • ν := isMulLeftInvariant_eq_smul_of_innerRegular _ _
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 : C = 1
rwa : ∀ (hC : map (⇑f : (a : G) → H) μ = HSMul.hSMul (α := ℝ≥0) 1 ν) (this : C = 1), map (⇑f : (a : G) → H) μ = ν
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hC : map (⇑f : (a : G) → H) μ = ν) (this : C = 1), map (⇑f : (a : G) → H) μ = ν
⊢ map (⇑f : (a : G) → H) μ = ν

Tactic:
rwa [this, one_smul] at hC

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • ν
suffices : C = 1
⊢ map (⇑f : (a : G) → H) μ = ν

Tactic:
suffices C = 1 by rwa [this, one_smul] at hC
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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∞)
rw₇ rw₈ : Eq (α := ℝ≥0∞) ((ν : (a : Set H) → ℝ≥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∞)

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

Premises used: ENNReal.smul_def, MeasureTheory.Measure.map_apply, Continuous.measurable, MeasureTheory.Measure.smul_apply, Set.preimage_univ, smul_eq_mul, one_mul, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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 • ν
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : C = 1), C = 1
⊢ C = 1

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

Premises used: ENNReal.coe_eq_one, MeasureTheory.measure_ne_top, ENNReal.mul_left_inj, NeZero.ne
-- 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
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 : μ.Regular
c : ℝ≥0∞ := (↑(μ.inv.haarScalarFactor μ) : ℝ≥0∞)
⊢ μ.inv = c • μ

Tactic:
have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_regular μ.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 : μ.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 • μ
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 : μ.Regular
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 : μ.Regular
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 : μ.Regular
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 : μ.Regular
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 : μ.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_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 : μ.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
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]