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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
rw : c • μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
rw₁ : c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
rw₂ rw₃ : μ'.haarScalarFactor μ = μ'.haarScalarFactor μ
⊢ (c • μ').haarScalarFactor (c • μ) = μ'.haarScalarFactor μ

Tactic:
rw [haarScalarFactor_smul, smul_eq_mul, mul_haarScalarFactor_smul _ _ hc]

Premises used: MeasureTheory.Measure.haarScalarFactor_smul, smul_eq_mul, MeasureTheory.Measure.mul_haarScalarFactor_smul
-- 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
pos : ∀ (hG : LocallyCompactSpace G), μ.haarScalarFactor μ = 1
neg : ∀ (hG : ¬LocallyCompactSpace G), μ.haarScalarFactor μ = 1
⊢ μ.haarScalarFactor μ = 1

Tactic:
by_cases hG : 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
hG : ¬LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1

Tactic:
simp [haarScalarFactor, hG]

Premises used: 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
hG : LocallyCompactSpace G
pos :
  ∀ (g : C(G, ℝ))
    (hg :
      HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
        LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
    μ.haarScalarFactor μ = 1
⊢ μ.haarScalarFactor μ = 1

Tactic:
obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)

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
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0

Tactic:
have int_g_ne_zero : ∫ x, g x ∂μ ≠ 0 :=
    ne_of_gt (g.2.integral_pos_of_hasCompactSupport_nonneg_nonzero hg.1 hg.2.1 hg.2.2)
-- 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
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_ne_zero : Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0
pos : (↑(μ.haarScalarFactor μ) : ℝ) = (↑1 : ℝ)
⊢ μ.haarScalarFactor μ = 1

Tactic:
apply NNReal.coe_injective

Premises used: NNReal.coe_injective
-- 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
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_ne_zero : Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0
⊢ (↑(μ.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)

Tactic:
haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg

Premises used: MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_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 : μ.IsHaarMeasure
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_ne_zero : Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0
⊢ HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) = 1

Tactic:
div_self int_g_ne_zero

Premises used: div_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 : μ.IsHaarMeasure
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_ne_zero : Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0
⊢ (↑(μ.haarScalarFactor μ) : ℝ) = (↑1 : ℝ)

Tactic:
calc
    haarScalarFactor μ μ = (∫ x, g x ∂μ) / ∫ x, g x ∂μ :=
      haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg
    _ = 1 := div_self int_g_ne_zero

Premises used: MeasureTheory.integral, MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, DFunLike.coe, MeasureTheory.Measure.haarScalarFactor, div_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 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
pos : ∀ (hG : LocallyCompactSpace G), μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
neg : ∀ (hG : ¬LocallyCompactSpace G), μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

Tactic:
by_cases hG : 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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : ¬LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

Tactic:
simp [haarScalarFactor, hG]

Premises used: 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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)),
    μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
⊢ Eq (α := ℝ) (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ'.haarScalarFactor μ • μ)

Tactic:
have Z := integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ g_cont g_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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z : Eq (α := ℝ) (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ'.haarScalarFactor μ • μ)
⊢ HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)

Tactic:
simp only [integral_smul_nnreal_measure, smul_smul,
    integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' ν g_cont g_comp,
    integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ ν g_cont g_comp] at Z

Premises used: MeasureTheory.integral_smul_nnreal_measure, smul_smul, MeasureTheory.Measure.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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
apply :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞)
        (support (M := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont })) :
      ℝ≥0∞)
apply₁ : Integrable (ε := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν
⊢ LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)

Tactic:
apply (integral_pos_iff_support_of_nonneg g_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 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞)
        (support (M := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont })) :
      ℝ≥0∞)

Tactic:
IsOpen.measure_pos ν g_cont.isOpen_support ⟨1, g_one⟩

Premises used: IsOpen.measure_pos, Continuous.isOpen_support, 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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞)
        (support (M := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont })) :
      ℝ≥0∞)

Tactic:
exact IsOpen.measure_pos ν g_cont.isOpen_support ⟨1, g_one⟩

Premises used: IsOpen.measure_pos, Continuous.isOpen_support, 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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ Integrable (ε := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν

Tactic:
g_cont.integrable_of_hasCompactSupport g_comp

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 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ Integrable (ε := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν

Tactic:
exact g_cont.integrable_of_hasCompactSupport g_comp

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 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)

Tactic:
have int_g_pos : 0 < ∫ x, g x ∂ν := by
    apply (integral_pos_iff_support_of_nonneg g_nonneg _).2
    · exact IsOpen.measure_pos ν g_cont.isOpen_support ⟨1, g_one⟩
    · exact g_cont.integrable_of_hasCompactSupport g_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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)
⊢ (↑(μ'.haarScalarFactor ν) : ℝ) * ∫ (x : G), g x ∂ν =
    (↑(μ'.haarScalarFactor μ * μ.haarScalarFactor ν) : ℝ) * ∫ (x : G), g x ∂ν

Tactic:
change (haarScalarFactor μ' ν : ℝ) * ∫ (x : G), g x ∂ν =
    (haarScalarFactor μ' μ * haarScalarFactor μ ν : ℝ≥0) * ∫ (x : G), g x ∂ν at Z

Premises used: HMul.hMul, NNReal.toReal, 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 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : 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 ∂ν)
Z :
  (↑(μ'.haarScalarFactor ν) : ℝ) * ∫ (x : G), g x ∂ν =
    (↑(μ'.haarScalarFactor μ * μ.haarScalarFactor ν) : ℝ) * ∫ (x : G), g x ∂ν
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

Tactic:
simpa only [mul_eq_mul_right_iff (M₀ := ℝ), int_g_pos.ne', or_false, ← NNReal.eq_iff] using Z

Premises used: NNReal.eq_iff, mul_eq_mul_right_iff, LT.lt.ne', or_false
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
pos :
  ∀ (hG : LocallyCompactSpace G),
    haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
neg :
  ∀ (hG : ¬LocallyCompactSpace G),
    haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ

Tactic:
by_cases hG : 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : ¬LocallyCompactSpace G
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ

Tactic:
simp [haarScalarFactor, hG]

Premises used: 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
pos :
  ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f)
    (hf :
      HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
        LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
          Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
    haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ

Tactic:
obtain ⟨⟨f, f_cont⟩, hf⟩ := exists_continuous_nonneg_pos (1 : G)

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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0

Tactic:
have int_f_ne_zero : ∫ (x : G), f x ∂(map φ μ) ≠ 0 :=
    ne_of_gt (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero hf.1 hf.2.1 hf.2.2)
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ AEMeasurable (β := G) (⇑φ : (a : G) → G) μ'

Tactic:
fun_prop