awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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) ∂ν))
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have M : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
Tactic: have M n : ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂(haarScalarFactor μ' μ • μ) := by
    apply integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ (vf_cont n)
    apply h'f.comp_left
    simp only [v, thickenedIndicator_apply, NNReal.coe_eq_zero]
    rw [thickenedIndicatorAux_zero (u_mem n).1]
    · simp only [ENNReal.toNNReal_zero]
    · simpa using (u_mem n).2.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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 μ • μ)
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have I1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ') atTop
  (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
Tactic: have I1 := I μ' (by infer_instance)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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) ∂μ') atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have I1₁ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
  (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
Tactic: simp_rw [M] at I1
Cleared hypotheses: I1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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) ∂μ'))
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have J1 : 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))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
have h : ∀ (x : G), Eq (α := ℝ) (indicator {1} (fun (x : ℝ) ↦ 1) (f x)) ((f ⁻¹' {1}).indicator (fun (x : G) ↦ 1) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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})
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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
⊢ μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})
have mf : MeasurableSet (f ⁻¹' {1})
Tactic: have mf : MeasurableSet (f ⁻¹' {1}) := (isClosed_singleton.preimage hf).measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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 μ • μ)
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have J2 : μ'.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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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})
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have C : IsCompact (f ⁻¹' {1})
Tactic: have C : IsCompact (f ⁻¹' {1}) := h'f.isCompact_preimage hf isClosed_singleton (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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})
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have J2₁ : 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
Cleared hypotheses: J2, C
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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)
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ' : (a : Set G) → ℝ≥0∞) s
have apply : ∀ (r : ℝ≥0∞) (hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)),
  r < (μ' : (a : Set G) → ℝ≥0∞) s
Tactic: apply le_of_forall_lt (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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 μ • μ
⊢ r < (μ' : (a : Set G) → ℝ≥0∞) s
have this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have : ν s ≠ ∞ := ((measure_mono subset_closure).trans_lt h's.measure_lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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 < (μ' : (a : Set G) → ℝ≥0∞) s
have obtain : ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f) (f_comp : HasCompactSupport f) (hf : f ⁻¹' {1} ⊆ s)
  (νf : r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})), r < (μ' : (a : Set G) → ℝ≥0∞) s
Tactic: obtain ⟨-, hf, ⟨f, f_cont, f_comp, rfl⟩, νf⟩ :
      ∃ K ⊆ s, (∃ f, Continuous f ∧ HasCompactSupport f ∧ K = f ⁻¹' {1}) ∧ r < ν K :=
    innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group ⟨hs, this⟩ r
      (by convert! hr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have apply : (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm ?_ (smul_measure_isMulInvariant_le_of_isCompact_closure μ' μ hs h's)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have change : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: change μ' s ≤ ν s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have obtain : ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f)
  (hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s))
  (f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)),
  LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: obtain ⟨⟨f, f_cont⟩, hf, -, f_comp, -⟩ : ∃ f : C(G, ℝ), EqOn f 1 (closure s) ∧ EqOn f 0 ∅
      ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
    exists_continuous_one_zero_of_isCompact h's isClosed_empty (disjoint_empty _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have t_closed : IsClosed[inst] t
Tactic: have t_closed : IsClosed t := isClosed_singleton.preimage f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have t_comp : IsCompact t
Tactic: have t_comp : IsCompact t := f_comp.isCompact_preimage f_cont isClosed_singleton (by simp)