awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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, _] fun (a : G × G) ↦ g (a.2⁻¹ * a.1)

Tactic:
hg.comp (continuous_snd.inv.mul continuous_fst)

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.mul, Continuous.inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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, _] fun (a : G × G) ↦ g (a.2⁻¹ * a.1)

Tactic:
exact hg.comp (continuous_snd.inv.mul continuous_fst)

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.mul, Continuous.inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ IsCompact K

Tactic:
have K_comp : IsCompact K := h'f
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ IsCompact L

Tactic:
have L_comp : IsCompact L := h'g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ IsCompact M

Tactic:
have M_comp : IsCompact M :=
          (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ IsCompact (closure[inst] M)

Tactic:
have M'_comp : IsCompact (closure M) := M_comp.closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
pos : ∀ (H : x ∈ K), f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0
neg : ∀ (H : x ∉ K), f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0

Tactic:
by_cases H : x ∈ K
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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

Tactic:
simp [image_eq_zero_of_notMem_tsupport H]

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
hx : y⁻¹ * x ∉ tsupport g
⊢ g (y⁻¹ * x) = 0

Tactic:
apply image_eq_zero_of_notMem_tsupport

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
hx : ∀ (hxy : y⁻¹ * x ∈ tsupport g), (x, y) ∈ K ×ˢ closure[inst] M
⊢ y⁻¹ * x ∉ tsupport g

Tactic:
contrapose hxy
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
hx : y ∈ closure[inst] M
⊢ (x, y) ∈ K ×ˢ closure[inst] M

Tactic:
simp only [mem_prod, H, true_and]

Premises used: Set.mem_prod, true_and
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
hx : y ∈ M
⊢ y ∈ closure[inst] M

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
hx : ∃ (a : G) (b : G), (a ∈ K ∧ b ∈ L) ∧ a * b⁻¹ = y
⊢ y ∈ M

Tactic:
simp only [M, mem_image, mem_prod, Prod.exists]

Premises used: Set.mem_image, Set.mem_prod, Prod.exists
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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⁻¹ * x)⁻¹ = y

Tactic:
group
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ ∃ (a : G) (b : G), (a ∈ K ∧ b ∈ L) ∧ a * b⁻¹ = y

Tactic:
exact ⟨x, y⁻¹ * x, ⟨H, hxy⟩, by group⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ 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⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
this : g (y⁻¹ * x) = 0
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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)
⊢ ∀ 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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
apply : IsClosed[instTopologicalSpaceProd] (K ×ˢ closure[inst] M)
⊢ HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))

Tactic:
apply HasCompactSupport.intro' (K_comp.prod M'_comp) ?_ this

Premises used: IsCompact.prod, HasCompactSupport.intro'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ IsClosed[instTopologicalSpaceProd] (K ×ˢ closure[inst] M)

Tactic:
(isClosed_tsupport f).prod isClosed_closure

Premises used: IsClosed.prod, isClosed_tsupport, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
⊢ IsClosed[instTopologicalSpaceProd] (K ×ˢ closure[inst] M)

Tactic:
exact (isClosed_tsupport f).prod isClosed_closure

Premises used: IsClosed.prod, isClosed_tsupport, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
e_f : ∀ (y : G), Eq (α := ℝ) (∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ) (∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g 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 ∂μ ∂ν)

Tactic:
congr with y
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
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
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 ∂μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ) (∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ)

Tactic:
rw [← integral_mul_left_eq_self _ y]

Premises used: MeasureTheory.integral_mul_left_eq_self