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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
  (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)
Tactic: rw [hs.measure_eq_iSup_isCompact, hs.measure_eq_iSup_isCompact]
-- 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegular
inst_10 : μ'.InnerRegular
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)
have h : ∀ (K : Set G) (_Ks : K ⊆ s) (K_comp : IsCompact K),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: congr! 4 with K _Ks K_comp
-- 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
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
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
  (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)
Tactic: rw [hU.measure_eq_iSup_isCompact, hU.measure_eq_iSup_isCompact]
-- 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
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
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) K)
have h : ∀ (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: congr! 4 with K _KU K_comp
-- 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.Regular
inst_10 : μ'.Regular
⊢ μ' = μ'.haarScalarFactor μ • μ
have A : ∀ (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
-- 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
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
⊢ μ ≪ ν
have have : ∀ (K : PositiveCompacts G), μ ≪ ν
Tactic: have K : PositiveCompacts G := Classical.arbitrary _
-- 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
inst_5 : LocallyCompactSpace G
inst_6 : SecondCountableTopology G
μ ν : Measure G
inst_7 : SigmaFinite μ
inst_8 : μ.IsMulLeftInvariant
inst_9 : ν.IsHaarMeasure
K : PositiveCompacts G
⊢ μ ≪ ν
have h : haarMeasure K = (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) • ν
Tactic: have h : haarMeasure K = (haarScalarFactor (haarMeasure K) ν : ℝ≥0∞) • ν :=
    isMulLeftInvariant_eq_smul (haarMeasure K) ν
-- 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
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∞) • ν
⊢ μ ≪ ν
have rw : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑(haarScalarFactor (haarMeasure K) ν) : ℝ≥0∞) •
    ν ≪
  ν
Tactic: rw [haarMeasure_unique μ K, h, smul_smul]
-- 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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [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∞)
⊢ map (⇑f : (a : G) → H) μ = ν
have this : IsFiniteMeasure μ
Tactic: have : IsFiniteMeasure μ := ⟨by rw [huniv]; apply measure_lt_top⟩
-- 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 : IsFiniteMeasure μ
⊢ map (⇑f : (a : G) → H) μ = ν
have this₁ : IsHaarMeasure.{u_2} (G := H) (map (⇑f : (a : G) → H) μ)
Tactic: have : (μ.map f).IsHaarMeasure := isHaarMeasure_map_of_isFiniteMeasure μ f hcont hsurj
-- 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) μ) ν
⊢ map (⇑f : (a : G) → H) μ = ν
have hC : map (⇑f : (a : G) → H) μ = C • ν
Tactic: have hC : μ.map f = C • ν := isMulLeftInvariant_eq_smul_of_innerRegular _ _
-- 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 : C = 1
⊢ map (⇑f : (a : G) → H) μ = ν
have rwa : ∀ (hC : map (⇑f : (a : G) → H) μ = HSMul.hSMul (α := ℝ≥0) 1 ν) (this : C = 1), map (⇑f : (a : G) → H) μ = ν
Tactic: rwa [this, one_smul] at hC
Cleared hypotheses: hC, 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 : C = 1
rwa : ∀ (hC : map (⇑f : (a : G) → H) μ = HSMul.hSMul (α := ℝ≥0) 1 ν) (this : C = 1), map (⇑f : (a : G) → H) μ = ν
⊢ map (⇑f : (a : G) → H) μ = ν
have rwa₁ : ∀ (hC : map (⇑f : (a : G) → H) μ = ν) (this : C = 1), map (⇑f : (a : G) → H) μ = ν
Tactic: rwa [this, one_smul] at hC
Cleared hypotheses: hC, 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 : 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 • ν
⊢ map (⇑f : (a : G) → H) μ = ν
have suffices : C = 1
Tactic: suffices C = 1 by rwa [this, one_smul] at hC
-- 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 • ν
⊢ 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 : HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) = (ν : (a : Set H) → ℝ≥0∞) univ
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 (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
⊢ 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₁ : HSMul.hSMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) = (ν : (a : Set H) → ℝ≥0∞) univ
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 (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
⊢ 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₂ : HSMul.hSMul (β := ℝ≥0∞) C ((ν : (a : Set H) → ℝ≥0∞) univ : ℝ≥0∞) = (ν : (a : Set H) → ℝ≥0∞) univ
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 (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
⊢ 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∞) ((C • ν : (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 (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∞)
⊢ 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∞) (((map (⇑f : (a : G) → H) μ : Measure H) : (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 (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∞)
⊢ 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 G) → ℝ≥0∞) (preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) 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]