awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
a :
  HasCompactSupport (β := ℝ) fun (x : A) ↦
    f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x)
a₁ : Ne (α := ℝ) (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂ν) 0
⊢ HDiv.hDiv (α := ℝ) (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂μ)
      (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂ν) =
    (↑(μ.addHaarScalarFactor ν) : ℝ)

Tactic:
refine (addHaarScalarFactor_eq_integral_div _ _ (by fun_prop) ?_ ?_).symm

Premises used: MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
⊢ HasCompactSupport (β := ℝ) fun (x : A) ↦
    f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x)

Tactic:
f_comp.comp_isClosedEmbedding (Homeomorph.smul _).isClosedEmbedding

Premises used: HasCompactSupport.comp_isClosedEmbedding, Homeomorph.smul, Homeomorph.isClosedEmbedding
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
⊢ HasCompactSupport (β := ℝ) fun (x : A) ↦
    f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x)

Tactic:
exact f_comp.comp_isClosedEmbedding (Homeomorph.smul _).isClosedEmbedding

Premises used: HasCompactSupport.comp_isClosedEmbedding, Homeomorph.smul, Homeomorph.isClosedEmbedding
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
a : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
⊢ Ne (α := ℝ) (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂ν) 0

Tactic:
rw [← integral_domSMul]

Premises used: MeasureTheory.integral_domSMul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
⊢ Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0

Tactic:
(f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'

Premises used: Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
f : A → ℝ
f_cont : Continuous[inst_4, _] f
f_comp : HasCompactSupport (α := A) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ)
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont : C(A, ℝ) }
f_zero : Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(A, ℝ) } : (a : A) → ℝ) 0 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0
⊢ Ne (α := ℝ) (∫ (x : A), f x ∂g • ν) 0

Tactic:
exact (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'

Premises used: Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
rw : μ.addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
rw₁ : μ.addHaarScalarFactor (g • ν) * ν.addHaarScalarFactor μ = ν.addHaarScalarFactor (g • ν)
rw₂ : ν.addHaarScalarFactor μ * μ.addHaarScalarFactor (g • ν) = ν.addHaarScalarFactor (g • ν)
rw₃ rw₄ : ν.addHaarScalarFactor (g • ν) = ν.addHaarScalarFactor (g • ν)
⊢ μ.addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)

Tactic:
rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]

Premises used: MeasureTheory.Measure.addHaarScalarFactor_eq_mul, mul_comm, HSMul.hSMul, MeasureTheory.Measure.addHaarScalarFactor_domSMul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
rw : (g • μ).addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
rw₁ : μ.addHaarScalarFactor ν * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
rw₂ : (g • ν).addHaarScalarFactor μ * μ.addHaarScalarFactor ν = (g • ν).addHaarScalarFactor ν
rw₃ rw₄ : (g • ν).addHaarScalarFactor ν = (g • ν).addHaarScalarFactor ν
⊢ (g • μ).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν

Tactic:
rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]

Premises used: MeasureTheory.Measure.addHaarScalarFactor_eq_mul, mul_comm, HSMul.hSMul, MeasureTheory.Measure.addHaarScalarFactor_domSMul
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (f ω))
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L (𝓝 (∫⁻ (ω : Ω), (↑(f ω) : ℝ≥0∞) ∂μ))

Tactic:
tendsto_lintegral_filter_of_dominated_convergence (fun _ ↦ c)
    (Eventually.of_forall fun i ↦ (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
    (@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_

Premises used: ENNReal.ofNNReal, Continuous.comp, Filter.Eventually.of_forall, BoundedContinuousFunction.continuous, MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence, Continuous.measurable, MeasureTheory.lintegral_const_lt_top, ENNReal.continuous_coe, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (f ω))
refine_1 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ≤ (fun (x : Ω) ↦ (↑c : ℝ≥0∞)) a
refine_2 : ∀ᵐ (a : Ω) ∂μ, Tendsto (fun (n : ι) ↦ (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) L (𝓝 (↑(f a) : ℝ≥0∞))
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L (𝓝 (∫⁻ (ω : Ω), (↑(f ω) : ℝ≥0∞) ∂μ))

Tactic:
refine tendsto_lintegral_filter_of_dominated_convergence (fun _ ↦ c)
    (Eventually.of_forall fun i ↦ (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
    (@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_

Premises used: ENNReal.ofNNReal, Continuous.comp, Filter.Eventually.of_forall, BoundedContinuousFunction.continuous, MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence, Continuous.measurable, MeasureTheory.lintegral_const_lt_top, ENNReal.continuous_coe, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (f ω))
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ≤ (fun (x : Ω) ↦ (↑c : ℝ≥0∞)) a

Tactic:
simpa only [Function.comp_apply, ENNReal.coe_le_coe] using fs_le_const

Premises used: ENNReal.coe_le_coe, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun (n : ι) ↦ (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) L (𝓝 (↑(f a) : ℝ≥0∞))

Tactic:
simpa only [Function.comp_apply, ENNReal.tendsto_coe] using fs_lim

Premises used: ENNReal.tendsto_coe, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L
    (𝓝 (∫⁻ (ω : Ω), (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞) ∂μ))

Tactic:
tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim

Premises used: MeasureTheory.tendsto_lintegral_nn_filter_of_le_const
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
h : (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (ω : Ω), (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞) ∂μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)

Tactic:
convert! tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim

Premises used: MeasureTheory.tendsto_lintegral_nn_filter_of_le_const
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
ω : Ω
⊢ E.indicator (fun (x : Ω) ↦ 1) ω = (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞)

Tactic:
simp only [ENNReal.coe_indicator, ENNReal.coe_one]

Premises used: ENNReal.coe_one, ENNReal.coe_indicator
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
⊢ ∀ (ω : Ω), E.indicator (fun (x : Ω) ↦ 1) ω = (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞)

Tactic:
have aux : ∀ ω, indicator E (fun _ ↦ (1 : ℝ≥0∞)) ω = ↑(indicator E (fun _ ↦ (1 : ℝ≥0)) ω) :=
    fun ω ↦ by simp only [ENNReal.coe_indicator, ENNReal.coe_one]
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun (x : Ω) ↦ 1) ω = (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞)
h : (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (x : Ω) in E, 1 ∂μ
⊢ (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (ω : Ω), (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞) ∂μ

Tactic:
simp_rw [← aux, lintegral_indicator E_mble]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun (x : Ω) ↦ 1) ω = (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (x : Ω) in E, 1 ∂μ

Tactic:
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator fun (x : Ω) ↦ 1))
⊢ ∀ (x : Ω), Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (fs i : (a : Ω) → ℝ≥0) x) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) x))

Tactic:
rw [tendsto_pi_nhds] at fs_lim

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ (x : Ω), Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (fs i : (a : Ω) → ℝ≥0) x) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) x))
⊢ ∀ (ω : Ω), Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))

Tactic:
fun ω ↦ fs_lim ω
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ (x : Ω), Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ (fs i : (a : Ω) → ℝ≥0) x) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) x))
⊢ ∀ (ω : Ω), Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))

Tactic:
exact fun ω ↦ fs_lim ω
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator fun (x : Ω) ↦ 1))
⊢ ∀ (ω : Ω), Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))

Tactic:
have fs_lim' :
    ∀ ω, Tendsto (fun n : ℕ ↦ (fs n ω : ℝ≥0)) atTop (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω)) := by
    rw [tendsto_pi_nhds] at fs_lim
    exact fun ω ↦ fs_lim ω
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator fun (x : Ω) ↦ 1))
fs_lim' :
  ∀ (ω : Ω), Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)

Tactic:
apply measure_of_cont_bdd_of_tendsto_filter_indicator μ E_mble fs
    (Eventually.of_forall fun n ↦ Eventually.of_forall (fs_bdd n)) (Eventually.of_forall fs_lim')

Premises used: MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
apply :
  Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
    (𝓝 (F.indicator fun (x : Ω) ↦ 1))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)

Tactic:
apply measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurableSet
    (fun n ↦ thickenedIndicator (δs_pos n) F) fun n ω ↦ thickenedIndicator_le_one (δs_pos n) F ω

Premises used: MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator, thickenedIndicator, thickenedIndicator_le_one, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (β := (a : Ω) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ F) : (a : Ω) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun (x : Ω) ↦ 1))

Tactic:
have key := thickenedIndicator_tendsto_indicator_closure δs_pos δs_lim F
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key :
  Tendsto (β := (a : Ω) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ F) : (a : Ω) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun (x : Ω) ↦ 1))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (key :
      Tendsto (β := (a : Ω) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ F) : (a : Ω) → ℝ≥0)) atTop
        (𝓝 (F.indicator fun (x : Ω) ↦ 1))),
    Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
      (𝓝 (F.indicator fun (x : Ω) ↦ 1))
⊢ Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
    (𝓝 (F.indicator fun (x : Ω) ↦ 1))

Tactic:
rwa [F_closed.closure_eq] at key

Premises used: IsClosed.closure_eq