awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 : Ω) → ℝ)
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have f₀_ae_nns : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 : Ω) → ℝ)
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have aux : ∫ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have auxs : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have aux₁ : ∫ (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
Cleared hypotheses: aux, auxs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have auxs₁ : ∀ (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
Cleared hypotheses: aux, auxs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)))
have refine : 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)))
have 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 Ω)))
Tactic: rw [tendsto_iff_forall_lintegral_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 : Ω →ᵇ ℝ
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
have 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 Ω))))
Tactic: simp_rw [BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 : Ω →ᵇ ℝ
⊢ 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 Ω))))
have 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 Ω))))
Tactic: set f_pos := f.nnrealPart with _def_f_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ 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 Ω))))
have 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 Ω))))
Tactic: set f_neg := (-f).nnrealPart with _def_f_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
    (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 Ω))))
have tends_pos : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
tends_pos :
  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)
⊢ 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 Ω))))
have tends_neg : Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
  (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
Tactic: have tends_neg := (ENNReal.tendsto_toReal (f_neg.lintegral_lt_top_of_nnreal μ).ne).comp (h f_neg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
tends_pos :
  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)
tends_neg :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
⊢ 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 Ω))))
have aux : ∀ (g : Ω →ᵇ ℝ≥0),
  Eq.{u_2 + 1} (α := γ → ℝ)
    (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) fun (i : γ) ↦
    (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
Tactic: have aux :
    ∀ g : Ω →ᵇ ℝ≥0,
      (ENNReal.toReal ∘ fun i : γ ↦ ∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)) =
        fun i : γ ↦ (∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)).toReal :=
    fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
tends_pos :
  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)
tends_neg :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
⊢ 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 Ω))))
have tends_pos₁ : Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
  (𝓝 (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
Tactic: simp_rw [aux, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral] at tends_pos tends_neg
Cleared hypotheses: tends_pos, tends_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
tends_pos :
  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)
tends_neg :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
tends_pos₁ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
⊢ 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 Ω))))
have tends_neg₁ : Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
  (𝓝 (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
Tactic: simp_rw [aux, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral] at tends_pos tends_neg
Cleared hypotheses: tends_pos, tends_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
have rw : (∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))) ↔
  ∀ (f : Ω →ᵇ 𝕜),
    Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
Tactic: rw [tendsto_iff_forall_integral_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
have refine_1 : ∀
  (h :
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω))))
  (f : Ω →ᵇ 𝕜),
  Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
Tactic: refine ⟨fun h f ↦ ?_, fun h f ↦ ?_⟩