awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
⊢ p⁻¹ * x ∈ k⁻¹

Tactic:
simpa only [Set.mem_inv, mul_inv_rev, inv_inv] using subset_tsupport _ hx

Premises used: subset_tsupport, inv_inv, mul_inv_rev, Set.mem_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
⊢ ContinuousOn.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t

Tactic:
have A : ContinuousOn (fun (x : G) ↦ ∫ y, g (y⁻¹ * x) ∂μ) t := by
    apply continuousOn_integral_of_compact_support k'_comp
    · exact (hg.comp (continuous_snd.inv.mul continuous_fst)).continuousOn
    · intro p x hp hx
      contrapose! hx
      refine ⟨p, hp, p⁻¹ * x, ?_, by simp⟩
      simpa only [Set.mem_inv, mul_inv_rev, inv_inv] using subset_tsupport _ hx
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
A : ContinuousOn.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀

Tactic:
A.continuousAt ht

Premises used: ContinuousOn.continuousAt
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
A : ContinuousOn.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀

Tactic:
exact A.continuousAt ht

Premises used: ContinuousOn.continuousAt
-- 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
inl :
  ∀ (Hf : f = 0),
    ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
inr :
  ∀ (Hf : LocallyCompactSpace G),
    ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
⊢ ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)

Tactic:
rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf

Premises used: HasCompactSupport.eq_zero_or_locallyCompactSpace_of_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 : f = 0
⊢ ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)

Tactic:
simp [Hf]
-- 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) ∂ν
⊢ Continuous[inst, _] D

Tactic:
have D_cont : Continuous D := continuous_integral_apply_inv_mul hg 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
x : G
⊢ Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)

Tactic:
fun_prop
-- 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
x : G
⊢ Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)

Tactic:
have C : Continuous (fun y ↦ g (y⁻¹ * x)) := by fun_prop
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
apply : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (support (M := ℝ) fun (x_1 : G) ↦ g (x_1⁻¹ * x)) : ℝ≥0∞)
apply₁ : LE.le.{u_1} (α := G → ℝ) 0 fun (x_1 : G) ↦ g (x_1⁻¹ * x)
apply₂ : Integrable (ε := ℝ) (fun (x_1 : G) ↦ g (x_1⁻¹ * x)) ν
⊢ 0 < D x

Tactic:
apply (integral_pos_iff_support_of_nonneg _ _).2

Premises used: Iff.mpr, MeasureTheory.integral_pos_iff_support_of_nonneg
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
apply : Set.Nonempty.{u_1} (α := G) (support (M := ℝ) fun (y : G) ↦ g (y⁻¹ * x))
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (support (M := ℝ) fun (x_1 : G) ↦ g (x_1⁻¹ * x)) : ℝ≥0∞)

Tactic:
apply C.isOpen_support.measure_pos ν

Premises used: IsOpen.measure_pos, Continuous.isOpen_support
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
⊢ Membership.mem (γ := Set G) (support (M := ℝ) fun (y : G) ↦ g (y⁻¹ * x)) (x * x₀⁻¹)

Tactic:
simpa using g_pos
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
⊢ Set.Nonempty.{u_1} (α := G) (support (M := ℝ) fun (y : G) ↦ g (y⁻¹ * x))

Tactic:
exact ⟨x * x₀⁻¹, by simpa using g_pos⟩
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
⊢ LE.le.{u_1} (α := G → ℝ) 0 fun (x_1 : G) ↦ g (x_1⁻¹ * x)

Tactic:
fun y ↦ g_nonneg (y⁻¹ * x)

Premises used: HMul.hMul, Inv.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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
⊢ LE.le.{u_1} (α := G → ℝ) 0 fun (x_1 : G) ↦ g (x_1⁻¹ * x)

Tactic:
exact fun y ↦ g_nonneg (y⁻¹ * x)

Premises used: HMul.hMul, Inv.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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
apply : HasCompactSupport (β := ℝ) fun (y : G) ↦ g (y⁻¹ * x)
⊢ Integrable (ε := ℝ) (fun (x_1 : G) ↦ g (x_1⁻¹ * x)) ν

Tactic:
apply C.integrable_of_hasCompactSupport

Premises used: Continuous.integrable_of_hasCompactSupport
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
⊢ HasCompactSupport (β := ℝ) fun (y : G) ↦ g (y⁻¹ * x)

Tactic:
h'g.comp_homeomorph ((Homeomorph.inv G).trans (Homeomorph.mulRight x))

Premises used: Homeomorph.mulRight, HasCompactSupport.comp_homeomorph, Homeomorph.inv, Homeomorph.trans
-- 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
x : G
C : Continuous[inst, _] fun (y : G) ↦ g (y⁻¹ * x)
⊢ HasCompactSupport (β := ℝ) fun (y : G) ↦ g (y⁻¹ * x)

Tactic:
exact h'g.comp_homeomorph ((Homeomorph.inv G).trans (Homeomorph.mulRight x))

Premises used: Homeomorph.mulRight, HasCompactSupport.comp_homeomorph, Homeomorph.inv, Homeomorph.trans
-- 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
⊢ ∀ (x : G), 0 < D x

Tactic:
have D_pos : ∀ x, 0 < D x := by
    intro x
    have C : Continuous (fun y ↦ g (y⁻¹ * x)) := by fun_prop
    apply (integral_pos_iff_support_of_nonneg _ _).2
    · apply C.isOpen_support.measure_pos ν
      exact ⟨x * x₀⁻¹, by simpa using g_pos⟩
    · exact fun y ↦ g_nonneg (y⁻¹ * x)
    · apply C.integrable_of_hasCompactSupport
      exact h'g.comp_homeomorph ((Homeomorph.inv G).trans (Homeomorph.mulRight x))
-- 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 : ∀ (x : G), f x = f x * (D x)⁻¹ * D x
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ) (∫ (x : G), f x * (D x)⁻¹ * D x ∂μ)

Tactic:
congr with x
-- 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
x : G
e_f : f x = f x * ((D x)⁻¹ * D x)
e_f₁ : f x = f x * 1
e_f₂ e_f₃ : f x = f x
⊢ f x = f x * (D x)⁻¹ * D x

Tactic:
rw [mul_assoc, inv_mul_cancel₀ (D_pos x).ne', mul_one]

Premises used: mul_assoc, LT.lt.ne', mul_one, inv_mul_cancel₀
-- 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
simp_rw :
  Eq (α := ℝ) (∫ (x : G), f x * (∫ (y : G), g (y⁻¹ * x) ∂ν)⁻¹ * ∫ (y : G), g (y⁻¹ * x) ∂ν ∂μ)
    (∫ (x : G), ∫ (y : G), f x * (∫ (y : G), g (y⁻¹ * x) ∂ν)⁻¹ * g (y⁻¹ * x) ∂ν ∂μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x * (D x)⁻¹ * D x ∂μ) (∫ (x : G), ∫ (y : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂ν ∂μ)

Tactic:
simp_rw [D, integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- 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
hf₁ : Continuous[instTopologicalSpaceProd, _] (uncurry fun (x y : G) ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))
h'f₁ : HasCompactSupport.{u_1, 0} (α := G × G) (β := ℝ) (uncurry fun (x y : G) ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))
⊢ Eq (α := ℝ) (∫ (x : G), ∫ (y : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂ν ∂μ)
    (∫ (y : G), ∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ ∂ν)

Tactic:
apply integral_integral_swap_of_hasCompactSupport

Premises used: MeasureTheory.integral_integral_swap_of_hasCompactSupport
-- 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
hf₁ : Continuous[instTopologicalSpaceProd, _] fun (a : G × G) ↦ f a.1 * (D a.1)⁻¹
hf₂ : Continuous[instTopologicalSpaceProd, _] fun (a : G × G) ↦ g (a.2⁻¹ * a.1)
⊢ Continuous[instTopologicalSpaceProd, _] (uncurry fun (x y : G) ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))

Tactic:
apply Continuous.mul

Premises used: Continuous.mul
-- 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) ↦ f a.1 * (D a.1)⁻¹

Tactic:
(hf.comp continuous_fst).mul
            ((D_cont.comp continuous_fst).inv₀ (fun x ↦ (D_pos _).ne'))

Premises used: Continuous.comp, continuous_fst, Prod.fst, Continuous.mul, LT.lt.ne', 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) ↦ f a.1 * (D a.1)⁻¹

Tactic:
exact (hf.comp continuous_fst).mul
            ((D_cont.comp continuous_fst).inv₀ (fun x ↦ (D_pos _).ne'))

Premises used: Continuous.comp, continuous_fst, Prod.fst, Continuous.mul, LT.lt.ne', Continuous.inv₀