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 : 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
H : x ∈ K
hxy : y⁻¹ * x ∈ tsupport g
⊢ (x, y) ∈ K ×ˢ closure[inst] M
have hx : y ∈ closure[inst] M
Tactic: simp only [mem_prod, H, true_and]
-- 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)
x y : G
H : x ∈ K
hxy : y⁻¹ * x ∈ tsupport g
⊢ y ∈ closure[inst] M
have hx : y ∈ M
Tactic: apply subset_closure
-- 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)
x y : G
H : x ∈ K
hxy : y⁻¹ * x ∈ tsupport g
⊢ y ∈ M
have hx : ∃ (a : G) (b : G), (a ∈ K ∧ b ∈ L) ∧ a * b⁻¹ = y
Tactic: simp only [M, mem_image, mem_prod, Prod.exists]
-- 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) ∉ K ×ˢ closure[inst] M
H : x ∈ K
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0
have this : g (y⁻¹ * x) = 0
Tactic: have : g (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 ⟨x, y⁻¹ * x, ⟨H, hxy⟩, 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 x * (D x)⁻¹ * g (y⁻¹ * x))
have this : ∀ p ∉ K ×ˢ closure[inst] M, f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0
Tactic: have : ∀ (p : G × G), p ∉ K ×ˢ closure M → f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0 := by
          rintro ⟨x, y⟩ hxy
          by_cases H : x ∈ K; swap
          · simp [image_eq_zero_of_notMem_tsupport H]
          have : g (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 ⟨x, y⁻¹ * x, ⟨H, hxy⟩, 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 ∉ K ×ˢ closure[inst] M, f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))
have apply : IsClosed[instTopologicalSpaceProd] (K ×ˢ closure[inst] M)
Tactic: apply HasCompactSupport.intro' (K_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 (α := ℝ) (∫ (y : G), ∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ ∂ν)
    (∫ (y : G), ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ ∂ν)
have e_f : ∀ (y : G), Eq (α := ℝ) (∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ) (∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ)
Tactic: congr with y
-- 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
y : G
⊢ Eq (α := ℝ) (∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ) (∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ)
have e_f : Eq (α := ℝ) (∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g (y⁻¹ * (y * x)) ∂μ)
  (∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ)
Tactic: rw [← integral_mul_left_eq_self _ y]
-- 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 (α := ℝ) (∫ (y : G), ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ ∂ν)
    (∫ (x : G), ∫ (y : G), f (y * x) * (D (y * x))⁻¹ * g x ∂ν ∂μ)
have apply : Continuous[instTopologicalSpaceProd, _] (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
Tactic: apply (integral_integral_swap_of_hasCompactSupport _ _).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
μ ν : 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
apply : Continuous[instTopologicalSpaceProd, _] (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
⊢ Eq (α := ℝ) (∫ (y : G), ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ ∂ν)
    (∫ (x : G), ∫ (y : G), f (y * x) * (D (y * x))⁻¹ * g x ∂ν ∂μ)
have apply₁ : HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
Tactic: apply (integral_integral_swap_of_hasCompactSupport _ _).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
μ ν : 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
⊢ Continuous[instTopologicalSpaceProd, _] (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have apply : Continuous[instTopologicalSpaceProd, _] fun (a : G × G) ↦ f (a.2 * a.1) * (D (a.2 * a.1))⁻¹
Tactic: apply Continuous.mul ?_ (hg.comp continuous_fst)
-- 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
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have K_comp : IsCompact K
Tactic: have K_comp : IsCompact K := 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 : 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
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have L_comp : IsCompact L
Tactic: have L_comp : IsCompact L := h'g
-- 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
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have M_comp : IsCompact M
Tactic: have M_comp : IsCompact M :=
          (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
-- 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
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f (y * x) * (D (y * x))⁻¹ * g x)
have M'_comp : IsCompact (closure[inst] M)
Tactic: have M'_comp : IsCompact (closure M) := M_comp.closure
-- 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)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst] M
⊢ f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0
have pos : ∀ (H : x ∈ L), f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0
Tactic: by_cases H : x ∈ L
-- 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)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst] M
pos : ∀ (H : x ∈ L), f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0
⊢ f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0
have neg : ∀ (H : x ∉ L), f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0
Tactic: by_cases H : x ∈ L
-- 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)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst] M
H : x ∈ L
⊢ f (y * x) = 0
have hx : y * x ∉ tsupport f
Tactic: apply image_eq_zero_of_notMem_tsupport
-- 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)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst] M
H : x ∈ L
⊢ y * x ∉ tsupport f
have hx : ∀ (hxy : y * x ∈ tsupport f), (x, y) ∈ L ×ˢ closure[inst] M
Tactic: contrapose hxy
Cleared hypotheses: hxy
-- 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)
x y : G
H : x ∈ L
hxy : y * x ∈ tsupport f
⊢ (x, y) ∈ L ×ˢ closure[inst] M
have hx : y ∈ closure[inst] M
Tactic: simp only [mem_prod, H, true_and]
-- 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)
x y : G
H : x ∈ L
hxy : y * x ∈ tsupport f
⊢ y ∈ closure[inst] M
have hx : y ∈ M
Tactic: apply subset_closure
-- 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)
x y : G
H : x ∈ L
hxy : y * x ∈ tsupport f
⊢ y ∈ M
have hx : ∃ (a : G) (b : G), (a ∈ K ∧ b ∈ L) ∧ a * b⁻¹ = y
Tactic: simp only [M, mem_image, mem_prod, Prod.exists]