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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
⊢ IsFiniteMeasureOnCompacts (μ'.haarScalarFactor μ • μ)

Tactic:
infer_instance
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
⊢ Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)

Tactic:
have J1 : ∫ (x : G), indicator {1} (fun _ ↦ (1 : ℝ)) (f x) ∂μ'
      = ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂(haarScalarFactor μ' μ • μ) :=
    tendsto_nhds_unique I1 (I (haarScalarFactor μ' μ • μ) (by infer_instance))
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
h : ∀ (x : G), Eq (α := ℝ) (indicator {1} (fun (x : ℝ) ↦ 1) (f x)) ((f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x)
⊢ Eq.{u_1 + 1} (α := (x : G) → ℝ) (fun (x : G) ↦ indicator {1} (fun (x : ℝ) ↦ 1) (f x)) fun (x : G) ↦
    (f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x

Tactic:
ext 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 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
x : G
⊢ Eq (α := ℝ) (indicator {1} (fun (x : ℝ) ↦ 1) (f x)) ((f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x)

Tactic:
(indicator_comp_right f (s := ({1} : Set ℝ)) (g := (fun _ ↦ (1 : ℝ))) (x := x)).symm

Premises used: Set.indicator_comp_right, 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
x : G
⊢ Eq (α := ℝ) (indicator {1} (fun (x : ℝ) ↦ 1) (f x)) ((f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x)

Tactic:
exact (indicator_comp_right f (s := ({1} : Set ℝ)) (g := (fun _ ↦ (1 : ℝ))) (x := x)).symm

Premises used: Set.indicator_comp_right, 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
⊢ Eq.{u_1 + 1} (α := (x : G) → ℝ) (fun (x : G) ↦ indicator {1} (fun (x : ℝ) ↦ 1) (f x)) fun (x : G) ↦
    (f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x

Tactic:
have : (fun x ↦ indicator {1} (fun _ ↦ (1 : ℝ)) (f x)) =
        (fun x ↦ indicator (f ⁻¹' {1}) (fun _ ↦ (1 : ℝ)) x) := by
      ext x
      exact (indicator_comp_right f (s := ({1} : Set ℝ)) (g := (fun _ ↦ (1 : ℝ))) (x := x)).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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
this :
  Eq.{u_1 + 1} (α := (x : G) → ℝ) (fun (x : G) ↦ indicator {1} (fun (x : ℝ) ↦ 1) (f x)) fun (x : G) ↦
    (f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x
⊢ MeasurableSet (f ⁻¹' {1})

Tactic:
have mf : MeasurableSet (f ⁻¹' {1}) := (isClosed_singleton.preimage hf).measurableSet
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
this :
  Eq.{u_1 + 1} (α := (x : G) → ℝ) (fun (x : G) ↦ indicator {1} (fun (x : ℝ) ↦ 1) (f x)) fun (x : G) ↦
    (f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x
mf : MeasurableSet (f ⁻¹' {1})
⊢ μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})

Tactic:
simpa only [this, mf, integral_indicator_const, smul_eq_mul, mul_one, Pi.smul_apply,
      nnreal_smul_coe_apply, ENNReal.toReal_mul, ENNReal.coe_toReal] using J1

Premises used: ENNReal.coe_toReal, MeasureTheory.Measure.nnreal_smul_coe_apply, ENNReal.toReal_mul, MeasureTheory.integral_indicator_const, smul_eq_mul, mul_one, Pi.smul_apply
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
⊢ μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})

Tactic:
have J2 : μ'.real (f ⁻¹' {1})
      = (haarScalarFactor μ' μ • μ).real (f ⁻¹' {1}) := by
    have : (fun x ↦ indicator {1} (fun _ ↦ (1 : ℝ)) (f x)) =
        (fun x ↦ indicator (f ⁻¹' {1}) (fun _ ↦ (1 : ℝ)) x) := by
      ext x
      exact (indicator_comp_right f (s := ({1} : Set ℝ)) (g := (fun _ ↦ (1 : ℝ))) (x := x)).symm
    have mf : MeasurableSet (f ⁻¹' {1}) := (isClosed_singleton.preimage hf).measurableSet
    simpa only [this, mf, integral_indicator_const, smul_eq_mul, mul_one, Pi.smul_apply,
      nnreal_smul_coe_apply, ENNReal.toReal_mul, ENNReal.coe_toReal] using J1
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
J2 : μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})
⊢ 0 ∉ {1}

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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
J2 : μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})
⊢ IsCompact (f ⁻¹' {1})

Tactic:
have C : IsCompact (f ⁻¹' {1}) := h'f.isCompact_preimage hf isClosed_singleton (by 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
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
J2 : μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})
C : IsCompact (f ⁻¹' {1})
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
    ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)

Tactic:
rw [measureReal_eq_measureReal_iff C.measure_lt_top.ne C.measure_lt_top.ne] at J2

Premises used: MeasureTheory.measureReal_eq_measureReal_iff, IsCompact.measure_lt_top, LT.lt.ne
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
J2 : μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})
C : IsCompact (f ⁻¹' {1})
J2₁ :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
    ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
⊢ IsCompact (f ⁻¹' {1})

Tactic:
rw [measureReal_eq_measureReal_iff C.measure_lt_top.ne C.measure_lt_top.ne] at J2

Premises used: MeasureTheory.measureReal_eq_measureReal_iff, IsCompact.measure_lt_top, LT.lt.ne
-- 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
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
        (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
I1 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
J1 :
  Eq (α := ℝ) (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ')
    (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ)
J2 :
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
    ((μ'.haarScalarFactor μ • μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
C : IsCompact (f ⁻¹' {1})
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)

Tactic:
simpa using J2
-- 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
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
apply :
  ∀ (r : ℝ≥0∞) (hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)),
    r < (μ' : (a : Set G) → ℝ≥0∞) s
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ' : (a : Set G) → ℝ≥0∞) s

Tactic:
apply le_of_forall_lt (fun r hr ↦ ?_)

Premises used: le_of_forall_lt
-- 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
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : ν s ≠ ∞ := ((measure_mono subset_closure).trans_lt h's.measure_lt_top).ne
-- 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
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
hr