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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ AEStronglyMeasurable (α := G) (β := ℝ) (m₀ := inst_3)
    (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) (map (⇑φ : (a : G) → G) μ')

Tactic:
fun_prop
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ AEMeasurable (β := G) (⇑φ : (a : G) → G) μ

Tactic:
fun_prop
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ AEStronglyMeasurable (α := G) (β := ℝ) (m₀ := inst_3)
    (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) (map (⇑φ : (a : G) → G) μ)

Tactic:
fun_prop
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
pos :
  HDiv.hDiv (α := ℝ)
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ')
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ')
      (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ)
pos₁ : HasCompactSupport (α := G) (f ∘ (⇑φ.toHomeomorph : (a : G) → G))
pos₂ : Ne (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ) 0
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ

Tactic:
rw [← NNReal.coe_inj, haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hf,
    haarScalarFactor_eq_integral_div μ' μ (f_cont.comp φ.continuous),
    integral_map (by fun_prop) (by fun_prop),
    integral_map (by fun_prop) (by fun_prop)]

Premises used: Homeomorph.continuous, MeasureTheory.integral_map, Continuous.comp, MeasureTheory.Measure.haarScalarFactor_eq_integral_div, ContinuousMulEquiv.toHomeomorph, MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, NNReal.coe_inj
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ HDiv.hDiv (α := ℝ)
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ')
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ')
      (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ)

Tactic:
rfl
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ HasCompactSupport (α := G) (f ∘ (⇑φ.toHomeomorph : (a : G) → G))

Tactic:
hf.1.comp_homeomorph φ.toHomeomorph

Premises used: HasCompactSupport.comp_homeomorph, And.left, ContinuousMulEquiv.toHomeomorph
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ HasCompactSupport (α := G) (f ∘ (⇑φ.toHomeomorph : (a : G) → G))

Tactic:
exact hf.1.comp_homeomorph φ.toHomeomorph

Premises used: HasCompactSupport.comp_homeomorph, And.left, ContinuousMulEquiv.toHomeomorph
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
pos : Ne (α := ℝ) (∫ (x : G), f ((φ : (a : G) → G) x) ∂μ) 0
⊢ Ne (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ) 0

Tactic:
change ∫ x, f (φ x) ∂μ ≠ 0
-- 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 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero pos pos₁ pos₂ pos₃ : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (y : G) ↦ f y) 0
⊢ Ne (α := ℝ) (∫ (x : G), f ((φ : (a : G) → G) x) ∂μ) 0

Tactic:
rwa [← integral_map (by fun_prop) f_cont.aestronglyMeasurable]

Premises used: MeasureTheory.integral_map, Continuous.aestronglyMeasurable
-- 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 : μ'.IsHaarMeasure
H : μ'.haarScalarFactor μ = 0
⊢ False

Tactic:
simpa [H] using haarScalarFactor_eq_mul μ' μ μ'

Premises used: MeasureTheory.Measure.haarScalarFactor_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
⊢ ∃ (u : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ) < 1)

Premises used: exists_seq_strictAnti_tendsto', zero_lt_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
obtain :
  ∀ (u : ℕ → ℝ) (u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)) (u_lim : Tendsto u atTop (𝓝 0)),
    (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
      HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)

Tactic:
obtain ⟨u, -, u_mem, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 1)
    ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ) < 1)

Premises used: exists_seq_strictAnti_tendsto', zero_lt_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) : ℝ)
n : ℕ
apply :
  Continuous[_, induced Subtype.val PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(thickenedIndicator ⋯ {1}) : (a : ℝ) → ℝ≥0)
⊢ Continuous[inst, _] (v n ∘ f)

Tactic:
apply Continuous.comp (continuous_induced_dom.comp ?_) hf

Premises used: Continuous.comp, continuous_induced_dom
-- 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) : ℝ)
n : ℕ
⊢ Continuous[_, induced Subtype.val PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(thickenedIndicator ⋯ {1}) : (a : ℝ) → ℝ≥0)

Tactic:
BoundedContinuousFunction.continuous (thickenedIndicator (u_mem n).left {1})

Premises used: thickenedIndicator, NNReal, BoundedContinuousFunction.continuous, And.left, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : 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) : ℝ)
n : ℕ
⊢ Continuous[_, induced Subtype.val PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(thickenedIndicator ⋯ {1}) : (a : ℝ) → ℝ≥0)

Tactic:
exact BoundedContinuousFunction.continuous (thickenedIndicator (u_mem n).left {1})

Premises used: thickenedIndicator, BoundedContinuousFunction.continuous, And.left, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : 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) : ℝ)
⊢ ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)

Tactic:
have vf_cont n : Continuous ((v n) ∘ f) := by
    apply Continuous.comp (continuous_induced_dom.comp ?_) hf
    exact BoundedContinuousFunction.continuous (thickenedIndicator (u_mem n).left {1})
-- 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 ν
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
h_lim : ∀ᵐ (a : G) ∂ν, Tendsto (β := ℝ) (fun (n : ℕ) ↦ v n (f a)) atTop (𝓝 (indicator {1} (fun (x : ℝ) ↦ 1) (f a)))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : G), v n (f x) ∂ν) atTop
    (𝓝 (∫ (x : G), indicator {1} (fun (x : ℝ) ↦ 1) (f x) ∂ν))

Tactic:
apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))

Premises used: Set.indicator, MeasureTheory.tendsto_integral_of_dominated_convergence, tsupport, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : 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 : ℕ), AEStronglyMeasurable (β := ℝ) (fun (a : G) ↦ v n (f a)) ν

Tactic:
fun n ↦ (vf_cont n).aestronglyMeasurable

Premises used: Continuous.aestronglyMeasurable, NNReal.toReal
-- 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 : ℕ), AEStronglyMeasurable (β := ℝ) (fun (a : G) ↦ v n (f a)) ν

Tactic:
exact fun n ↦ (vf_cont n).aestronglyMeasurable

Premises used: Continuous.aestronglyMeasurable
-- 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 ν
apply : IntegrableOn (ε := ℝ) (fun (x : G) ↦ 1) (tsupport f) ν
⊢ Integrable (ε := ℝ) ((tsupport f).indicator fun (x : G) ↦ 1) ν

Tactic:
apply IntegrableOn.integrable_indicator _ (isClosed_tsupport f).measurableSet

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, IsClosed.measurableSet, isClosed_tsupport
-- 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 ν
⊢ IntegrableOn (ε := ℝ) (fun (x : G) ↦ 1) (tsupport f) ν

Tactic:
simpa using IsCompact.measure_lt_top h'f

Premises used: IsCompact.measure_lt_top
-- 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 : ℕ), ∀ᵐ (a : G) ∂ν, ‖v n (f a)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) a

Tactic:
fun n ↦ Eventually.of_forall (fun x ↦ ?_)

Premises used: Filter.Eventually.of_forall
-- 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_bound : ∀ (n : ℕ) (x : G), ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
⊢ ∀ (n : ℕ), ∀ᵐ (a : G) ∂ν, ‖v n (f a)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) a

Tactic:
refine fun n ↦ Eventually.of_forall (fun x ↦ ?_)

Premises used: Filter.Eventually.of_forall
-- 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
pos : ∀ (hx : x ∈ tsupport f), ‖v n (f x)‖ ≤ (tsupport f).indicator (fun (x : G) ↦ 1) x
neg : ∀ (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

Tactic:
by_cases hx : x ∈ tsupport f

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

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

Premises used: Set.indicator_of_mem, NNReal.abs_eq, Real.norm_eq_abs