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
x : G
rw : (∫ (x_1 : G), f (x_1 * x) * (D (x_1 * x))⁻¹ ∂ν) * g x
| (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x

Tactic:
rw [← integral_mul_right_eq_self _ x]

Premises used: MeasureTheory.integral_mul_right_eq_self
-- 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
conv_rhs : (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x = (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x
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
⊢ (∫ (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]

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

Tactic:
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 : μ.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 • μ)
neg :
  ∀ (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 • μ)

Tactic:
by_cases H : LocallyCompactSpace G

Premises used: LocallyCompactSpace
-- 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 : μ.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 • μ)

Tactic:
⟨0, fun f f_cont f_comp ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
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 μ)
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)

Tactic:
refine ⟨0, fun f f_cont f_comp ↦ ?_⟩
-- 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 : μ.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 μ)
neg₁ : ∀ (hf : LocallyCompactSpace G), 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 μ)

Tactic:
rcases f_comp.eq_zero_or_locallyCompactSpace_of_group f_cont 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : f = 0
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)

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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : LocallyCompactSpace G
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)

Tactic:
(H hf).elim

Premises used: False.elim
-- 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : LocallyCompactSpace G
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂HSMul.hSMul (α := ℝ≥0) 0 μ)

Tactic:
exact (H hf).elim

Premises used: False.elim
-- 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
⊢ ∃ (g : C(G, ℝ)),
    HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧ 0 ≤ g ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)

Tactic:
exists_continuous_nonneg_pos 1

Premises used: exists_continuous_nonneg_pos, OfNat.ofNat
-- 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
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 • μ)
⊢ ∃ (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

Premises used: exists_continuous_nonneg_pos, OfNat.ofNat
-- 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 : μ.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 : ℝ)
⊢ 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
-- 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 : μ.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 ∂μ')
⊢ 0 ≤ c

Tactic:
have c_nonneg : 0 ≤ c :=
    mul_nonneg (inv_nonneg.2 (integral_nonneg g_nonneg)) (integral_nonneg g_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 : μ.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 • μ)

Tactic:
⟨.mk c c_nonneg, fun f f_cont f_comp ↦ ?_⟩

Premises used: NNReal.mk, Exists.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 : μ.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
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 • μ)
⊢ ∃ (c : ℝ≥0),
    ∀ (f : G → ℝ),
      Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ)

Tactic:
refine ⟨.mk c c_nonneg, fun f f_cont f_comp ↦ ?_⟩
-- 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 : μ.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
⊢ ∫ (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
-- 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 : μ.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 ∂μ)
⊢ 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

Premises used: LT.lt.ne', mul_inv_eq_iff_eq_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 : μ.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) ∂ν)⁻¹ ∂ν
⊢ ∫ (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
-- 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 : μ.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 ∂μ')
⊢ ∫ (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

Premises used: mul_assoc, mul_comm
-- 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 : μ.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 (α := ℝ) (∫ (x : G), g x ∂μ)⁻¹ (∫ (x : G), g x ∂μ') * ∫ (x : G), f x ∂μ
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ)

Tactic:
simp [B, integral_smul_nnreal_measure, c, NNReal.smul_def]

Premises used: MeasureTheory.integral_smul_nnreal_measure, NNReal.smul_def
-- 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 : μ.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 μ • μ)
inr : ∀ (Hf : LocallyCompactSpace G), Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)

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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
Hf : f = 0
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)

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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
Hf : LocallyCompactSpace G
inr :
  Eq (α := ℝ) (∫ (x : G), f x ∂μ')
    (∫ (x : G),
      f
        x ∂Exists.choose (p := fun (c : ℝ≥0) ↦
          ∀ (f : G → ℝ),
            Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ))
          ⋯ •
        μ)
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)

Tactic:
simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]

Premises used: ite_false, not_true_eq_false, MeasureTheory.Measure.haarScalarFactor
-- 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
Hf : LocallyCompactSpace G
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ')
    (∫ (x : G),
      f
        x ∂Exists.choose (p := fun (c : ℝ≥0) ↦
          ∀ (f : G → ℝ),
            Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ))
          ⋯ •
        μ)

Tactic:
(exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose_spec
      f hf h'f

Premises used: Exists.choose_spec, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
Hf : LocallyCompactSpace G
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ')
    (∫ (x : G),
      f
        x ∂Exists.choose (p := fun (c : ℝ≥0) ↦
          ∀ (f : G → ℝ),
            Continuous[inst, _] f → HasCompactSupport f → Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂c • μ))
          ⋯ •
        μ)

Tactic:
exact (exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose_spec
      f hf h'f

Premises used: Exists.choose_spec, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport