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 : μ.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 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:
classical
  rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
  · simp [Hf]
  · simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]
    exact (exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ).choose_spec
      f hf h'f

Premises used: Exists.choose_spec, ite_false, HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group, not_true_eq_false, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, 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
int_nonzero : Ne (α := ℝ) (∫ (x : G), f x ∂μ) 0
⊢ Eq (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ)

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

Tactic:
rw [integral_smul_nnreal_measure] at this

Premises used: MeasureTheory.integral_smul_nnreal_measure
-- 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
int_nonzero : Ne (α := ℝ) (∫ (x : G), f x ∂μ) 0
this : ∫ (x : G), f x ∂μ' = HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ) (∫ (x : G), f x ∂μ)
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) = HDiv.hDiv (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ)

Tactic:
EuclideanDomain.eq_div_of_mul_eq_left int_nonzero this.symm

Premises used: EuclideanDomain.eq_div_of_mul_eq_left, Eq.symm
-- 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
int_nonzero : Ne (α := ℝ) (∫ (x : G), f x ∂μ) 0
this : ∫ (x : G), f x ∂μ' = HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ) (∫ (x : G), f x ∂μ)
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) = HDiv.hDiv (α := ℝ) (∫ (x : G), f x ∂μ') (∫ (x : G), f x ∂μ)

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left int_nonzero this.symm

Premises used: EuclideanDomain.eq_div_of_mul_eq_left, Eq.symm
-- 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 : C(G, ℝ)
hf : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)

Tactic:
obtain ⟨f_comp, f_nonneg, f_one⟩ := 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 : C(G, ℝ)
hf : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
⊢ 0 ≤ f

Tactic:
obtain ⟨f_comp, f_nonneg, f_one⟩ := 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 : C(G, ℝ)
hf : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧ 0 ≤ f ∧ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
f_nonneg : 0 ≤ f
⊢ Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)

Tactic:
obtain ⟨f_comp, f_nonneg, f_one⟩ := 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 : C(G, ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
f_nonneg : 0 ≤ f
f_one : Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ) 0

Tactic:
have int_f_ne_zero : ∫ (x : G), f x ∂μ ≠ 0 :=
    ne_of_gt (f.2.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_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
f : C(G, ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
f_nonneg : 0 ≤ f
f_one : Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ) 0
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ') (∫ (x : G), (f : (a : G) → ℝ) x ∂μ)

Tactic:
haarScalarFactor_eq_integral_div _ _ f.2 f_comp int_f_ne_zero

Premises used: MeasureTheory.Measure.haarScalarFactor_eq_integral_div, ContinuousMap.continuous_toFun
-- 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 : C(G, ℝ)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ)
f_nonneg : 0 ≤ f
f_one : Ne (α := ℝ) ((f : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ) 0
⊢ (↑(μ'.haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f : (a : G) → ℝ) x ∂μ') (∫ (x : G), (f : (a : G) → ℝ) x ∂μ)

Tactic:
exact haarScalarFactor_eq_integral_div _ _ f.2 f_comp int_f_ne_zero

Premises used: MeasureTheory.Measure.haarScalarFactor_eq_integral_div, ContinuousMap.continuous_toFun
-- 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
obtain :
  ∀ (g : C(G, ℝ))
    (hg :
      HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
        LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
    (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ

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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
a : (↑((c • μ').haarScalarFactor μ) : ℝ) = (↑(c • μ'.haarScalarFactor μ) : ℝ)
⊢ (c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ

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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑((c • μ').haarScalarFactor μ) : ℝ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ') (∫ (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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ∫ (x : G), (g : (a : G) → ℝ) x ∂μ

Tactic:
simp
-- 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
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ∫ (x : G), (g : (a : G) → ℝ) x ∂μ =
    c • HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)

Tactic:
smul_div_assoc c _ _

Premises used: smul_div_assoc
-- 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
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
rw rw₁ : c • (↑(μ'.haarScalarFactor μ) : ℝ) = c • (↑(μ'.haarScalarFactor μ) : ℝ)
⊢ c • HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    c • (↑(μ'.haarScalarFactor μ) : ℝ)

Tactic:
rw [← 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
haarScalarFactor :
  HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ∫ (x : G), (g : (a : G) → ℝ) x ∂μ
haarScalarFactor₁ :
  c • HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    c • (↑(μ'.haarScalarFactor μ) : ℝ)
⊢ (↑((c • μ').haarScalarFactor μ) : ℝ) = (↑(c • μ'.haarScalarFactor μ) : ℝ)

Tactic:
calc
    haarScalarFactor (c • μ') μ = (∫ x, g x ∂(c • μ')) / ∫ x, g x ∂μ :=
      haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg
    _ = (c • (∫ x, g x ∂μ')) / ∫ x, g x ∂μ := by simp
    _ = c • ((∫ x, g x ∂μ') / ∫ x, g x ∂μ) := smul_div_assoc c _ _
    _ = c • haarScalarFactor μ' μ := by
      rw [← haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]

Premises used: HDiv.hDiv, smul_div_assoc, MeasureTheory.integral, HSMul.hSMul, MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, DFunLike.coe, 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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
⊢ (c • μ).IsHaarMeasure

Tactic:
have : IsHaarMeasure (c • μ) := IsHaarMeasure.nnreal_smul _ hc
-- 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
this : (c • μ).IsHaarMeasure
obtain :
  ∀ (g : C(G, ℝ))
    (hg :
      HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
        LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
    c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ

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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
a : (↑(c * μ'.haarScalarFactor (c • μ)) : ℝ) = (↑(μ'.haarScalarFactor μ) : ℝ)
⊢ c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ

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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
rw rw₁ :
  (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ) =
    (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
⊢ (↑c : ℝ) * (↑(μ'.haarScalarFactor (c • μ)) : ℝ) =
    (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)

Tactic:
rw [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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ) =
    (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ))

Tactic:
simp
-- 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
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
rw :
  ((↑c : ℝ) * ∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ((↑c : ℝ) * ∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)
⊢ (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)

Tactic:
rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]

Premises used: mul_div_assoc, NNReal.smul_def, smul_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
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ (↑c : ℝ) ≠ 0

Tactic:
simp [hc]
-- 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
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ ((↑c : ℝ) * ∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / ((↑c : ℝ) * ∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)

Tactic:
exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])

Premises used: MeasureTheory.integral, mul_div_mul_left, DFunLike.coe
-- 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
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) =
    (↑(μ'.haarScalarFactor μ) : ℝ)

Tactic:
(haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg).symm

Premises used: MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, Eq.symm
-- 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
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
c₁ :
  (↑c : ℝ) * (↑(μ'.haarScalarFactor (c • μ)) : ℝ) =
    (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ)
c₂ :
  (↑c : ℝ) * HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂c • μ) =
    (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ))
c₃ :
  (↑c : ℝ) * ((∫ (x : G), (g : (a : G) → ℝ) x ∂μ') / HSMul.hSMul (β := ℝ) c (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ') (∫ (x : G), (g : (a : G) → ℝ) x ∂μ)
⊢ (↑(c * μ'.haarScalarFactor (c • μ)) : ℝ) = (↑(μ'.haarScalarFactor μ) : ℝ)

Tactic:
calc
    c * haarScalarFactor μ' (c • μ) = c * ((∫ x, g x ∂μ') / ∫ x, g x ∂(c • μ)) := by
      rw [haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg]
    _ = c * ((∫ x, g x ∂μ') / (c • ∫ x, g x ∂μ)) := by simp
    _ = (∫ x, g x ∂μ') / (∫ x, g x ∂μ) := by
      rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
      exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])
    _ = μ'.haarScalarFactor μ :=
      (haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hg).symm

Premises used: HDiv.hDiv, MeasureTheory.integral, HSMul.hSMul, MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, Eq.symm, DFunLike.coe, MeasureTheory.Measure.haarScalarFactor