awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 • μ
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 : μ.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 • μ
⊢ 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 : μ.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 • μ
⊢ 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 : μ.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 • μ
⊢ 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 : μ.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 • μ
⊢ 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 : μ.InnerRegular
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 : μ.InnerRegular
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 : μ.InnerRegular
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 : μ.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 = μ
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 : μ.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 (α := ℝ≥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 : μ.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∞)
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 : μ.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
⊢ μ.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 : μ.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∞)
⊢ μ.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 : μ.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
⊢ μ.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 : μ.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 = μ
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 : μ.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 = μ
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 : μ.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 = μ
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
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ᵈᵐᵃ
⊢ (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν
have 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 ν
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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 : ℝ)
⊢ (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν
have int_f_ne_zero : 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
⊢ (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν
have a : (↑((g • μ).addHaarScalarFactor (g • ν)) : ℝ) = (↑(μ.addHaarScalarFactor ν) : ℝ)
Tactic: apply NNReal.coe_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
⊢ (↑((g • μ).addHaarScalarFactor (g • ν)) : ℝ) = (↑(μ.addHaarScalarFactor ν) : ℝ)
have 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 ν) : ℝ)
Tactic: rw [addHaarScalarFactor_eq_integral_div (g • μ) (g • ν) f_cont f_comp int_f_ne_zero,
    integral_domSMul, integral_domSMul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
⊢ 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 ν) : ℝ)
have a : HasCompactSupport (β := ℝ) fun (x : A) ↦
  f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x)
Tactic: refine (addHaarScalarFactor_eq_integral_div _ _ (by fun_prop) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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 :
  HasCompactSupport (β := ℝ) fun (x : A) ↦
    f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x)
⊢ 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 ν) : ℝ)
have a₁ : Ne (α := ℝ) (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂ν) 0
Tactic: refine (addHaarScalarFactor_eq_integral_div _ _ (by fun_prop) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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ᵈᵐᵃ
⊢ μ.addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
have rw : μ.addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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ᵈᵐᵃ
rw : μ.addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
⊢ μ.addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
have rw₁ : μ.addHaarScalarFactor (g • ν) * ν.addHaarScalarFactor μ = ν.addHaarScalarFactor (g • ν)
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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ᵈᵐᵃ
rw : μ.addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
rw₁ : μ.addHaarScalarFactor (g • ν) * ν.addHaarScalarFactor μ = ν.addHaarScalarFactor (g • ν)
⊢ μ.addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
have rw₂ : ν.addHaarScalarFactor μ * μ.addHaarScalarFactor (g • ν) = ν.addHaarScalarFactor (g • ν)
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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ᵈᵐᵃ
rw : μ.addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
rw₁ : μ.addHaarScalarFactor (g • ν) * ν.addHaarScalarFactor μ = ν.addHaarScalarFactor (g • ν)
rw₂ : ν.addHaarScalarFactor μ * μ.addHaarScalarFactor (g • ν) = ν.addHaarScalarFactor (g • ν)
⊢ μ.addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
have rw₃ : ν.addHaarScalarFactor (g • ν) = ν.addHaarScalarFactor (g • ν)
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]