awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂(↑μ : Measure Ω), (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim :
  ∀ᵐ (ω : Ω) ∂(↑μ : Measure Ω),
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((fs i : (a : Ω) → ℝ≥0) ω : ℝ≥0)) L (𝓝 ((f : (a : Ω) → ℝ≥0) ω) : Filter ℝ≥0)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
tendsto_lintegral_nn_filter_of_le_const (Ω := Ω) μ fs_le_const fs_lim

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

Tactic:
exact tendsto_lintegral_nn_filter_of_le_const (Ω := Ω) μ fs_le_const fs_lim

Premises used: MeasureTheory.FiniteMeasure.toMeasure, MeasureTheory.tendsto_lintegral_nn_filter_of_le_const
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
fs : ℕ → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim :
  ∀ (ω : Ω),
    Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ((fs n : (a : Ω) → ℝ≥0) ω : ℝ≥0)) atTop (𝓝 ((f : (a : Ω) → ℝ≥0) ω) : Filter ℝ≥0)
⊢ Tendsto (fun (n : ℕ) ↦ μ.testAgainstNN (fs n)) atTop (𝓝 (μ.testAgainstNN f))

Tactic:
tendsto_testAgainstNN_filter_of_le_const
    (.of_forall fun n ↦ .of_forall (fs_le_const n))
    (.of_forall fs_lim)

Premises used: Filter.Eventually.of_forall, MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
apply :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ)

Tactic:
apply tendsto_iff_forall_lintegral_tendsto.mpr

Premises used: Iff.mpr, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
apply :
  Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
⊢ Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
apply (ENNReal.tendsto_toReal_iff (fi := F)
      (fun i ↦ (f.lintegral_lt_top_of_nnreal (μs i)).ne) (f.lintegral_lt_top_of_nnreal μ).ne).mp

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal, Iff.mp, ENNReal.tendsto_toReal_iff, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
⊢ LipschitzWith 1 NNReal.toReal

Tactic:
have lip : LipschitzWith 1 ((↑) : ℝ≥0 → ℝ) := NNReal.isometry_coe.lipschitz
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
⊢ let f₀ := comp NNReal.toReal lip f;
  f₀ = comp NNReal.toReal lip f

Tactic:
set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀

Premises used: BoundedContinuousFunction.comp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
⊢ Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))

Tactic:
have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
x : Ω
⊢ LE.le (α := (fun (a : Ω) ↦ ℝ) x) (0 x : ℝ) ((f₀ : (a : Ω) → ℝ) x : ℝ)

Tactic:
simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]

Premises used: Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
⊢ LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)

Tactic:
have f₀_nn : 0 ≤ ⇑f₀ := fun _ ↦ by
    simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
⊢ (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)

Tactic:
have f₀_ae_nn : 0 ≤ᵐ[(μ : Measure Ω)] ⇑f₀ := .of_forall f₀_nn
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
⊢ ∀ (i : γ), (ae (↑(μs i) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)

Tactic:
have f₀_ae_nns : ∀ i, 0 ≤ᵐ[(μs i : Measure Ω)] ⇑f₀ := fun i ↦ .of_forall f₀_nn
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nns : ∀ (i : γ), (ae (↑(μs i) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
⊢ ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑μ : Measure Ω)).toReal

Tactic:
have aux :=
    integral_eq_lintegral_of_nonneg_ae f₀_ae_nn f₀.continuous.measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nns : ∀ (i : γ), (ae (↑(μs i) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
aux :
  ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑μ : Measure Ω)).toReal
⊢ ∀ (i : γ),
    ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑(μs i) : Measure Ω) =
      (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑(μs i) : Measure Ω)).toReal

Tactic:
have auxs := fun i ↦
    integral_eq_lintegral_of_nonneg_ae (f₀_ae_nns i) f₀.continuous.measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nns : ∀ (i : γ), (ae (↑(μs i) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
aux :
  ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑μ : Measure Ω)).toReal
auxs :
  ∀ (i : γ),
    ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑(μs i) : Measure Ω) =
      (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑(μs i) : Measure Ω)).toReal
⊢ ∫ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ) ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal

Tactic:
simp_rw [f₀_eq, Function.comp_apply, ENNReal.ofReal_coe_nnreal] at aux auxs

Premises used: ENNReal.ofReal_coe_nnreal, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nns : ∀ (i : γ), (ae (↑(μs i) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
aux :
  ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑μ : Measure Ω)).toReal
auxs :
  ∀ (i : γ),
    ∫ (a : Ω), (f₀ : (a : Ω) → ℝ) a ∂(↑(μs i) : Measure Ω) =
      (∫⁻ (a : Ω), ENNReal.ofReal ((f₀ : (a : Ω) → ℝ) a) ∂(↑(μs i) : Measure Ω)).toReal
aux₁ :
  ∫ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ) ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal
⊢ ∀ (i : γ),
    ∫ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ) ∂(↑(μs i) : Measure Ω) =
      (∫⁻ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal

Tactic:
simp_rw [f₀_eq, Function.comp_apply, ENNReal.ofReal_coe_nnreal] at aux auxs

Premises used: ENNReal.ofReal_coe_nnreal, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
f₀_ae_nns : ∀ (i : γ), (ae (↑(μs i) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
aux :
  ∫ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ) ∂(↑μ : Measure Ω) =
    (∫⁻ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal
auxs :
  ∀ (i : γ),
    ∫ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ) ∂(↑(μs i) : Measure Ω) =
      (∫⁻ (a : Ω), (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)

Tactic:
simpa only [← aux, ← auxs] using h f₀
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))

Tactic:
⟨?_, tendsto_of_forall_integral_tendsto⟩

Premises used: Iff.intro, MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
refine :
  Tendsto μs F (𝓝 μ) →
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))

Tactic:
refine ⟨?_, tendsto_of_forall_integral_tendsto⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
rw :
  (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))) →
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ) →
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))

Tactic:
rw [tendsto_iff_forall_lintegral_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
simp_rw :
  Tendsto
    (fun (i : γ) ↦
      HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f.nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
        (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
    F
    (𝓝
      (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f.nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
        (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))

Tactic:
simp_rw [BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub]

Premises used: BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
set :
  let f_pos := f.nnrealPart;
  ∀ (_def_f_pos : f_pos = f.nnrealPart),
    Tendsto
      (fun (i : γ) ↦
        HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
          (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
      F
      (𝓝
        (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
          (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))
⊢ Tendsto
    (fun (i : γ) ↦
      HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f.nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
        (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
    F
    (𝓝
      (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f.nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
        (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))

Tactic:
set f_pos := f.nnrealPart with _def_f_pos

Premises used: BoundedContinuousFunction.nnrealPart
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
set :
  let f_neg := (-f).nnrealPart;
  ∀ (_def_f_neg : f_neg = (-f).nnrealPart),
    Tendsto
      (fun (i : γ) ↦
        HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
          (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
      F
      (𝓝
        (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
          (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))
⊢ Tendsto
    (fun (i : γ) ↦
      HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
        (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
    F
    (𝓝
      (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
        (∫ (x : Ω), (↑(((-f).nnrealPart : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))

Tactic:
set f_neg := (-f).nnrealPart with _def_f_neg

Premises used: BoundedContinuousFunction.nnrealPart, Neg.neg
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
⊢ Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)

Tactic:
have tends_pos := (ENNReal.tendsto_toReal (f_pos.lintegral_lt_top_of_nnreal μ).ne).comp (h f_pos)