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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∈ tsupport f
⊢ LE.le (α := ℝ≥0) ((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x) : ℝ≥0) (1 : ℝ≥0)

Tactic:
thickenedIndicator_le_one _ _ _

Premises used: thickenedIndicator_le_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 : 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
⊢ LE.le (α := ℝ≥0) ((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x) : ℝ≥0) (1 : ℝ≥0)

Tactic:
exact thickenedIndicator_le_one _ _ _

Premises used: thickenedIndicator_le_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 : 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 : (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x)) : ℝ) ≤ 0
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x

Tactic:
simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, not_false_eq_true, indicator_of_notMem]

Premises used: NNReal.abs_eq, Set.indicator_of_notMem, not_false_eq_true, Real.norm_eq_abs
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
neg : (↑0 : ℝ) ≤ 0
neg₁ : f x ∉ Metric.thickening (u n) {1}
⊢ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) (f x)) : ℝ) ≤ 0

Tactic:
rw [thickenedIndicator_zero]

Premises used: thickenedIndicator_zero
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
⊢ (↑0 : ℝ) ≤ 0

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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
⊢ f x ∉ Metric.thickening (u n) {1}

Tactic:
simpa [image_eq_zero_of_notMem_tsupport hx] using (u_mem n).2.le

Premises used: image_eq_zero_of_notMem_tsupport, LT.lt.le, And.right
-- 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
h_lim : ∀ (x : G), Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f x)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))
⊢ ∀ᵐ (a : G) ∂ν, Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f a)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f a)))

Tactic:
filter_upwards with 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)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
x : G
⊢ Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (thickenedIndicator ⋯ {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)
-- 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)
ν : 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 (β := ℝ≥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

Premises used: closure_singleton, thickenedIndicator_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)
ν : 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 (a : ℕ) ↦ (↑(thickenedIndicatorAux (u a) {1} (f x)).toNNReal : ℝ)) atTop
    (𝓝 (↑(indicator {1} (fun (x : ℝ) ↦ 1) (f x)) : ℝ))

Tactic:
NNReal.tendsto_coe.2 T

Premises used: Iff.mpr, NNReal.tendsto_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
μ' μ : 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)))
h : indicator {1} (fun (x : ℝ) ↦ 1) (f x) = (↑(indicator {1} (fun (x : ℝ) ↦ 1) (f x)) : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f x)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f x)))

Tactic:
convert! NNReal.tendsto_coe.2 T

Premises used: Iff.mpr, NNReal.tendsto_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
μ' μ : 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)))
⊢ indicator {1} (fun (x : ℝ) ↦ 1) (f x) = (↑(indicator {1} (fun (x : ℝ) ↦ 1) (f 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
μ' μ : 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),
    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
-- 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) ∂ν))
n : ℕ
apply : HasCompactSupport (v n ∘ f)
⊢ Eq (α := ℝ) (∫ (x : G), v n (f x) ∂μ') (∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ)

Tactic:
apply integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ (vf_cont n)

Premises used: MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : 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 : ℕ
apply : v n 0 = 0
⊢ HasCompactSupport (v n ∘ f)

Tactic:
apply h'f.comp_left

Premises used: HasCompactSupport.comp_left
-- 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) ∂ν))
n : ℕ
simp : (thickenedIndicatorAux (α := ℝ) (u n) {1} 0).toNNReal = 0
⊢ v n 0 = 0

Tactic:
simp only [v, thickenedIndicator_apply, NNReal.coe_eq_zero]

Premises used: NNReal.coe_eq_zero, thickenedIndicator_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) ∂ν))
n : ℕ
rw : ENNReal.toNNReal 0 = 0
x_out : 0 ∉ Metric.thickening (u n) {1}
⊢ (thickenedIndicatorAux (α := ℝ) (u n) {1} 0).toNNReal = 0

Tactic:
rw [thickenedIndicatorAux_zero (u_mem n).1]

Premises used: thickenedIndicatorAux_zero, And.left
-- 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) ∂ν))
n : ℕ
⊢ ENNReal.toNNReal 0 = 0

Tactic:
simp only [ENNReal.toNNReal_zero]

Premises used: ENNReal.toNNReal_zero
-- 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) ∂ν))
n : ℕ
⊢ 0 ∉ Metric.thickening (u n) {1}

Tactic:
simpa using (u_mem n).2.le

Premises used: LT.lt.le, And.right
-- 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) ∂ν))
⊢ ∀ (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
-- 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 μ • μ)
⊢ IsFiniteMeasureOnCompacts μ'

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 μ • μ)
⊢ 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)
-- 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) ∂μ') atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂μ'))
⊢ 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