awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst] M)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst] M
H : x ∈ L
⊢ f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0
have this : f (y * x) = 0
Tactic: have : f (y * x) = 0 := by
            apply image_eq_zero_of_notMem_tsupport
            contrapose hxy
            simp only [mem_prod, H, true_and]
            apply subset_closure
            simp only [M, mem_image, mem_prod, Prod.exists]
            exact ⟨y * x, x, ⟨hxy, H⟩, by group⟩
-- 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 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst] M)
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have this : ∀ p ∉ L ×ˢ closure[inst] M, f (p.2 * p.1) * (D (p.2 * p.1))⁻¹ * g p.1 = 0
Tactic: have : ∀ (p : G × G), p ∉ L ×ˢ closure M →
            f (p.2 * p.1) * (D (p.2 * p.1))⁻¹ * g p.1 = 0 := by
          rintro ⟨x, y⟩ hxy
          by_cases H : x ∈ L; swap
          · simp [image_eq_zero_of_notMem_tsupport H]
          have : f (y * x) = 0 := by
            apply image_eq_zero_of_notMem_tsupport
            contrapose hxy
            simp only [mem_prod, H, true_and]
            apply subset_closure
            simp only [M, mem_image, mem_prod, Prod.exists]
            exact ⟨y * x, x, ⟨hxy, H⟩, by group⟩
          simp [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
μ ν : Measure G
inst_5 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst] M)
this : ∀ p ∉ L ×ˢ closure[inst] M, f (p.2 * p.1) * (D (p.2 * p.1))⁻¹ * g p.1 = 0
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have apply : IsClosed[instTopologicalSpaceProd] (L ×ˢ closure[inst] M)
Tactic: apply HasCompactSupport.intro' (L_comp.prod M'_comp) ?_ 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
μ ν : Measure G
inst_5 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ Eq (α := ℝ) (∫ (x : G), ∫ (y : G), f (y * x) * (D (y * x))⁻¹ * g x ∂ν ∂μ)
    (∫ (x : G), (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x ∂μ)
have simp_rw : Eq (α := ℝ) (∫ (x : G), (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x ∂μ)
  (∫ (x : G), (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x ∂μ)
Tactic: simp_rw [integral_mul_const]
-- 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 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ Eq (α := ℝ) (∫ (x : G), (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x ∂μ)
    (∫ (x : G), (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x ∂μ)
have e_f : ∀ (x : G), (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
Tactic: congr with x
-- 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 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
x : G
| (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
have rw : (∫ (x_1 : G), f (x_1 * x) * (D (x_1 * x))⁻¹ ∂ν) * g x
Tactic: rw [← integral_mul_right_eq_self _ x]
-- 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 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
x : G
⊢ (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
have conv_rhs : (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
Tactic: conv_rhs => rw [← integral_mul_right_eq_self _ x]
-- 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 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst, _] D
D_pos : ∀ (x : G), 0 < D x
x : G
conv_rhs : (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
⊢ (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
have e_f : (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (x_1 : G), f (x_1 * x) * (D (x_1 * x))⁻¹ ∂ν) * g x
Tactic: conv_rhs => rw [← integral_mul_right_eq_self _ x]
-- 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
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have pos : ∀ (H : LocallyCompactSpace G),
  ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
Tactic: by_cases H : 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
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
pos :
  ∀ (H : LocallyCompactSpace G),
    ∃ (c : ℝ≥0),
      ∀ (f : G → ℝ),
        Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have neg : ∀ (H : ¬LocallyCompactSpace G),
  ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
Tactic: by_cases H : 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
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have neg : ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f) (f_comp : HasCompactSupport f),
  Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)
Tactic: refine ⟨0, fun f f_cont f_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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)
have neg : ∀ (hf : f = 0), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)
Tactic: rcases f_comp.eq_zero_or_locallyCompactSpace_of_group f_cont with hf | hf
-- 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
H : ¬LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
neg : ∀ (hf : f = 0), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)
have neg₁ : ∀ (hf : LocallyCompactSpace G), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)
Tactic: rcases f_comp.eq_zero_or_locallyCompactSpace_of_group f_cont with hf | hf
-- 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
H : LocallyCompactSpace G
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have pos : ∀ (g : G → ℝ) (g_cont : Continuous[inst, _] g)
  (g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ))
  (g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) })
  (g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
  ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
Tactic: obtain ⟨⟨g, g_cont⟩, g_comp, g_nonneg, g_one⟩ :
    ∃ (g : C(G, ℝ)), HasCompactSupport g ∧ 0 ≤ g ∧ g 1 ≠ 0 := exists_continuous_nonneg_pos 1
-- 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
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
Tactic: have int_g_pos : 0 < ∫ x, g x ∂μ :=
    g_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero g_comp g_nonneg g_one
-- 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
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
c : ℝ := HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ')
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have c_nonneg : 0 ≤ c
Tactic: have c_nonneg : 0 ≤ c :=
    mul_nonneg (inv_nonneg.2 (integral_nonneg g_nonneg)) (integral_nonneg g_nonneg)
-- 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
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
c : ℝ := HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ')
c_nonneg : 0 ≤ c
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)
have pos : ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f) (f_comp : HasCompactSupport f),
  Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ)
Tactic: refine ⟨.mk c c_nonneg, fun f f_cont f_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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
c : ℝ := HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ')
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ)
have A : ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
Tactic: have A : ∫ x, f x ∂μ = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ :=
    integral_isMulLeftInvariant_isMulRightInvariant_combo f_cont f_comp g_cont g_comp g_nonneg g_one
-- 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
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
c : ℝ := HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ')
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ)
have A₁ : HMul.hMul (α := ℝ) (∫ (x : G), f x ∂μ) (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
Tactic: rw [← mul_inv_eq_iff_eq_mul₀ int_g_pos.ne'] at A
Cleared hypotheses: A
-- 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
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
c : ℝ := HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ')
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : HMul.hMul (α := ℝ) (∫ (x : G), f x ∂μ) (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ)
have B : ∫ (x : G), f x ∂μ' = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ')
Tactic: have B : ∫ x, f x ∂μ' = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ' :=
    integral_isMulLeftInvariant_isMulRightInvariant_combo f_cont f_comp g_cont g_comp g_nonneg g_one
-- 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
H : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂μ)
c : ℝ := HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ')
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : HMul.hMul (α := ℝ) (∫ (x : G), f x ∂μ) (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
B : ∫ (x : G), f x ∂μ' = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ')
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ)
have B₁ : ∫ (x : G), f x ∂μ' = HMul.hMul (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ') * ∫ (x : G), f x ∂μ
Tactic: rw [← A, mul_assoc, mul_comm] at B
Cleared hypotheses: B
-- 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: rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
-- 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: rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf