awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
have F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (β := ℝ) (fun (a : G) ↦ v n (f a)) ν
Tactic: apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (β := ℝ) (fun (a : G) ↦ v n (f a)) ν
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
have bound_integrable : Integrable (ε := ℝ) ((tsupport f).indicator fun (x : G) ↦ 1) ν
Tactic: apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (β := ℝ) (fun (a : G) ↦ v n (f a)) ν
bound_integrable : Integrable (ε := ℝ) ((tsupport f).indicator fun (x : G) ↦ 1) ν
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
have h_bound : ∀ (n : ℕ), ∀ᵐ (a : G) ∂ν, ‖v n (f a)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) a
Tactic: apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (β := ℝ) (fun (a : G) ↦ v n (f a)) ν
bound_integrable : Integrable (ε := ℝ) ((tsupport f).indicator fun (x : G) ↦ 1) ν
h_bound : ∀ (n : ℕ), ∀ᵐ (a : G) ∂ν, ‖v n (f a)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) a
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
have h_lim : ∀ᵐ (a : G) ∂ν, Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f a)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f a)))
Tactic: apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
⊢ Integrable (ε := ℝ) ((tsupport f).indicator fun (x : G) ↦ 1) ν
have apply : IntegrableOn (ε := ℝ) (fun (x : G) ↦ 1) (tsupport f) ν
Tactic: apply IntegrableOn.integrable_indicator _ (isClosed_tsupport f).measurableSet
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
⊢ ∀ (n : ℕ), ∀ᵐ (a : G) ∂ν, ‖v n (f a)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) a
have h_bound : ∀ (n : ℕ) (x : G), ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
Tactic: refine fun n ↦ Eventually.of_forall (fun x ↦ ?_)
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
have pos : ∀ (hx : x ∈ tsupport f), ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
Tactic: by_cases hx : x ∈ tsupport f
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
pos : ∀ (hx : x ∈ tsupport f), ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
have neg : ∀ (hx : x ∉ tsupport f), ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
Tactic: by_cases hx : x ∈ tsupport f
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∈ tsupport f
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
have pos : (↑((thickenedIndicator sorry {1} : (a : ℝ) → ℝ≥0) (f x)) : ℝ) ≤ 1
Tactic: simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, indicator_of_mem]
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
have neg : (↑((thickenedIndicator sorry {1} : (a : ℝ) → ℝ≥0) (f x)) : ℝ) ≤ 0
Tactic: simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, not_false_eq_true, indicator_of_notMem]
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
⊢ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x)) : ℝ) ≤ 0
have neg : (↑0 : ℝ) ≤ 0
Tactic: rw [thickenedIndicator_zero]
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
neg : (↑0 : ℝ) ≤ 0
⊢ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x)) : ℝ) ≤ 0
have neg₁ : f x ∉ Metric.thickening (u n) {1}
Tactic: rw [thickenedIndicator_zero]
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
⊢ ∀ᵐ (a : G) ∂ν, Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f a)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f a)))
have h_lim : ∀ (x : G), Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f x)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
Tactic: filter_upwards with 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
x : G
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f x)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
have T : Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (thickenedIndicator sorry {1} : (a : ℝ) → ℝ≥0) (f x)) atTop
  (𝓝 (indicator (closure {1}) (fun (x : ℝ) ↦ 1) (f x)))
Tactic: have T := tendsto_pi_nhds.1 (thickenedIndicator_tendsto_indicator_closure
        (fun n ↦ (u_mem n).1) u_lim ({1} : Set ℝ)) (f 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
x : G
T :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x)) atTop
    (𝓝 (indicator (closure {1}) (fun (x : ℝ) ↦ 1) (f x)))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f x)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
have T₁ : Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (thickenedIndicatorAux (u i) {1} (f x)).toNNReal) atTop
  (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
Tactic: simp only [thickenedIndicator_apply, closure_singleton] at T
Cleared hypotheses: T
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
x : G
T :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (thickenedIndicatorAux (u i) {1} (f x)).toNNReal) atTop
    (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f x)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
have h : indicator {1} (fun (x : ℝ) ↦ 1) (f x) = (↑(indicator {1} (fun (x : ℝ) ↦ 1) (f x)) : ℝ)
Tactic: convert! NNReal.tendsto_coe.2 T
-- 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)
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have I : ∀ (ν : Measure G),
  IsFiniteMeasureOnCompacts ν →
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
      (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))
Tactic: have I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ x, v n (f x) ∂ν) atTop
      (𝓝 (∫ x, Set.indicator ({1} : Set ℝ) (fun _ ↦ 1) (f x) ∂ν)) := by
    intro ν hν
    apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
    · exact fun n ↦ (vf_cont n).aestronglyMeasurable
    · apply IntegrableOn.integrable_indicator _ (isClosed_tsupport f).measurableSet
      simpa using IsCompact.measure_lt_top h'f
    · refine fun n ↦ Eventually.of_forall (fun x ↦ ?_)
      by_cases hx : x ∈ tsupport f
      · simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, indicator_of_mem]
        norm_cast
        exact thickenedIndicator_le_one _ _ _
      · simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, not_false_eq_true, indicator_of_notMem]
        rw [thickenedIndicator_zero]
        · simp
        · simpa [image_eq_zero_of_notMem_tsupport hx] using (u_mem n).2.le
    · filter_upwards with x
      have T := tendsto_pi_nhds.1 (thickenedIndicator_tendsto_indicator_closure
        (fun n ↦ (u_mem n).1) u_lim ({1} : Set ℝ)) (f x)
      simp only [thickenedIndicator_apply, closure_singleton] at T
      convert! NNReal.tendsto_coe.2 T
      simp
-- 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) ∂ν))
n : ℕ
⊢ Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)
have apply : HasCompactSupport (v n ∘ f)
Tactic: apply integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ (vf_cont n)
-- 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) ∂ν))
n : ℕ
⊢ HasCompactSupport (v n ∘ f)
have apply : v n 0 = 0
Tactic: apply h'f.comp_left
-- 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) ∂ν))
n : ℕ
⊢ v n 0 = 0
have simp : (thickenedIndicatorAux (α := ℝ) (u n) {1} 0).toNNReal = 0
Tactic: simp only [v, thickenedIndicator_apply, NNReal.coe_eq_zero]
-- 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) ∂ν))
n : ℕ
⊢ (thickenedIndicatorAux (α := ℝ) (u n) {1} 0).toNNReal = 0
have rw : ENNReal.toNNReal 0 = 0
Tactic: rw [thickenedIndicatorAux_zero (u_mem n).1]
-- 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) ∂ν))
n : ℕ
rw : ENNReal.toNNReal 0 = 0
⊢ (thickenedIndicatorAux (α := ℝ) (u n) {1} 0).toNNReal = 0
have x_out : 0 ∉ Metric.thickening (u n) {1}
Tactic: rw [thickenedIndicatorAux_zero (u_mem n).1]