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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
Hf : LocallyCompactSpace G
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
have inr : Eq (α := ℝ) (∫ (x : G), f x ∂μ')
  (∫ (x : G),
    f
      x ∂Exists.choose (p := fun (c : ℝ≥0) ↦
        ∀ (f : G → ℝ),
          Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ))
        sorry •
      μ)
Tactic: simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
have inl : ∀ (Hf : f = 0), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
Tactic: classical
  rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
  · simp [Hf]
  · simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]
    exact (exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose_spec
      f hf h'f
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
inl : ∀ (Hf : f = 0), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
have inr : ∀ (Hf : LocallyCompactSpace G), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
Tactic: classical
  rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
  · simp [Hf]
  · simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]
    exact (exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose_spec
      f hf h'f
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
int_nonzero : Ne (α := ℝ) (∫ (x : G), f x ∂μ) 0
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) = HDiv.hDiv (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ)
have this : Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
Tactic: have := integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ hf h'f
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
int_nonzero : Ne (α := ℝ) (∫ (x : G), f x ∂μ) 0
this : Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) = HDiv.hDiv (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ)
have this₁ : ∫ (x : G), f x ∂μ' = HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ) (∫ (x : G), f x ∂μ)
Tactic: rw [integral_smul_nnreal_measure] at this
Cleared hypotheses: this
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : C(G, ℝ)
hf : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ') (∫ (x : G), (f : (a : G) → ℝ) x ∂μ)
have f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
Tactic: obtain ⟨f_comp, f_nonneg, f_one⟩ := hf
Cleared hypotheses: hf
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : C(G, ℝ)
hf : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ') (∫ (x : G), (f : (a : G) → ℝ) x ∂μ)
have f_nonneg : 0 ≤ f
Tactic: obtain ⟨f_comp, f_nonneg, f_one⟩ := hf
Cleared hypotheses: hf
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : C(G, ℝ)
hf : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
f_nonneg : 0 ≤ f
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ') (∫ (x : G), (f : (a : G) → ℝ) x ∂μ)
have f_one : Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
Tactic: obtain ⟨f_comp, f_nonneg, f_one⟩ := hf
Cleared hypotheses: hf
-- 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : C(G, ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
f_nonneg : 0 ≤ f
f_one : Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ') (∫ (x : G), (f : (a : G) → ℝ) x ∂μ)
have int_f_ne_zero : Ne (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ) 0
Tactic: have int_f_ne_zero : ∫ (x : G), f x ∂μ ≠ 0 :=
    ne_of_gt (f.2.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_one)
-- 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
c : ℝ≥0
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
have obtain : ∀ (g : C(G, ℝ))
  (hg :
    HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
      LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
  (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
Tactic: obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)
-- 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
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
have a : (↑((c • μ').haarScalarFactor μ) : ℝ) = (↑(c • μ'.haarScalarFactor μ) : ℝ)
Tactic: apply NNReal.coe_injective
-- 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
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ c • HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    c • (↑(μ'.haarScalarFactor μ) : ℝ)
have rw : c • (↑(μ'.haarScalarFactor μ) : ℝ) = c • (↑(μ'.haarScalarFactor μ) : ℝ)
Tactic: rw [← haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
-- 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
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑((c • μ').haarScalarFactor μ) : ℝ) = (↑(c • μ'.haarScalarFactor μ) : ℝ)
have haarScalarFactor : HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
  HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ∫ (x : G), (g : (a : G) → ℝ) x ∂μ
Tactic: calc
    haarScalarFactor (c • μ') μ = (∫ x, g x ∂(c • μ')) / ∫ x, g x ∂μ :=
      haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg
    _ = (c • (∫ x, g x ∂μ')) / ∫ x, g x ∂μ := by simp
    _ = c • ((∫ x, g x ∂μ') / ∫ x, g x ∂μ) := smul_div_assoc c _ _
    _ = c • haarScalarFactor μ' μ := by
      rw [← haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
-- 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
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
haarScalarFactor :
  HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ∫ (x : G), (g : (a : G) → ℝ) x ∂μ
⊢ (↑((c • μ').haarScalarFactor μ) : ℝ) = (↑(c • μ'.haarScalarFactor μ) : ℝ)
have haarScalarFactor₁ : c • HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
  c • (↑(μ'.haarScalarFactor μ) : ℝ)
Tactic: calc
    haarScalarFactor (c • μ') μ = (∫ x, g x ∂(c • μ')) / ∫ x, g x ∂μ :=
      haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg
    _ = (c • (∫ x, g x ∂μ')) / ∫ x, g x ∂μ := by simp
    _ = c • ((∫ x, g x ∂μ') / ∫ x, g x ∂μ) := smul_div_assoc c _ _
    _ = c • haarScalarFactor μ' μ := by
      rw [← haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
-- 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
c : ℝ≥0
hc : c ≠ 0
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
have this : (c • μ).IsHaarMeasure
Tactic: have : IsHaarMeasure (c • μ) := IsHaarMeasure.nnreal_smul _ 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
have obtain : ∀ (g : C(G, ℝ))
  (hg :
    HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
      LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
  c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
Tactic: obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)
-- 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
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
have a : (↑(c * μ'.haarScalarFactor (c • μ)) : ℝ) = (↑(μ'.haarScalarFactor μ) : ℝ)
Tactic: apply NNReal.coe_injective
-- 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
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑c : ℝ) * (↑(μ'.haarScalarFactor (c • μ)) : ℝ) =
    (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
have rw : (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ) =
  (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
Tactic: rw [haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
-- 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
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)
have rw : ((↑c : ℝ) * ∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ((↑c : ℝ) * ∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
  HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)
Tactic: rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
-- 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
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑(c * μ'.haarScalarFactor (c • μ)) : ℝ) = (↑(μ'.haarScalarFactor μ) : ℝ)
have c₁ : (↑c : ℝ) * (↑(μ'.haarScalarFactor (c • μ)) : ℝ) =
  (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
Tactic: calc
    c * haarScalarFactor μ' (c • μ) = c * ((∫ x, g x ∂μ') / ∫ x, g x ∂(c • μ)) := by
      rw [haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
    _ = c * ((∫ x, g x ∂μ') / (c • ∫ x, g x ∂μ)) := by simp
    _ = (∫ x, g x ∂μ') / (∫ x, g x ∂μ) := by
      rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
      exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])
    _ = μ'.haarScalarFactor μ :=
      (haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg).symm
-- 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
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
c₁ :
  (↑c : ℝ) * (↑(μ'.haarScalarFactor (c • μ)) : ℝ) =
    (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
⊢ (↑(c * μ'.haarScalarFactor (c • μ)) : ℝ) = (↑(μ'.haarScalarFactor μ) : ℝ)
have c₂ : (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ) =
  (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ))
Tactic: calc
    c * haarScalarFactor μ' (c • μ) = c * ((∫ x, g x ∂μ') / ∫ x, g x ∂(c • μ)) := by
      rw [haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
    _ = c * ((∫ x, g x ∂μ') / (c • ∫ x, g x ∂μ)) := by simp
    _ = (∫ x, g x ∂μ') / (∫ x, g x ∂μ) := by
      rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
      exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])
    _ = μ'.haarScalarFactor μ :=
      (haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg).symm
-- 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
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
c₁ :
  (↑c : ℝ) * (↑(μ'.haarScalarFactor (c • μ)) : ℝ) =
    (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
c₂ :
  (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ) =
    (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ))
⊢ (↑(c * μ'.haarScalarFactor (c • μ)) : ℝ) = (↑(μ'.haarScalarFactor μ) : ℝ)
have c₃ : (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)) =
  HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)
Tactic: calc
    c * haarScalarFactor μ' (c • μ) = c * ((∫ x, g x ∂μ') / ∫ x, g x ∂(c • μ)) := by
      rw [haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
    _ = c * ((∫ x, g x ∂μ') / (c • ∫ x, g x ∂μ)) := by simp
    _ = (∫ x, g x ∂μ') / (∫ x, g x ∂μ) := by
      rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
      exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])
    _ = μ'.haarScalarFactor μ :=
      (haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg).symm
-- 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
c : ℝ≥0
hc : c ≠ 0
⊢ (c • μ').haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
have rw : c • μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
Tactic: rw [haarScalarFactor_smul, smul_eq_mul, mul_haarScalarFactor_smul _ _ 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
rw : c • μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
⊢ (c • μ').haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
have rw₁ : c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
Tactic: rw [haarScalarFactor_smul, smul_eq_mul, mul_haarScalarFactor_smul _ _ 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
rw : c • μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
rw₁ : c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
⊢ (c • μ').haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
have rw₂ : μ'.haarScalarFactor μ = μ'.haarScalarFactor μ
Tactic: rw [haarScalarFactor_smul, smul_eq_mul, mul_haarScalarFactor_smul _ _ 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
μ : Measure G
inst_5 : μ.IsHaarMeasure
⊢ μ.haarScalarFactor μ = 1
have pos : ∀ (hG : LocallyCompactSpace G), μ.haarScalarFactor μ = 1
Tactic: by_cases hG : LocallyCompactSpace G
-- 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
μ : Measure G
inst_5 : μ.IsHaarMeasure
pos : ∀ (hG : LocallyCompactSpace G), μ.haarScalarFactor μ = 1
⊢ μ.haarScalarFactor μ = 1
have neg : ∀ (hG : ¬LocallyCompactSpace G), μ.haarScalarFactor μ = 1
Tactic: by_cases hG : LocallyCompactSpace G