awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ
this :
  limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
    ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have rwa : ∀ (key : ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
  (this :
    limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
      ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
  LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
Tactic: rwa [this, _root_.sub_le_sub_iff_left ‖f‖] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ
this :
  limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
    ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
rwa :
  ∀
    (key :
      ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
    (this :
      limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
        ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
    LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have rwa₁ : ∀
  (key :
    LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L))
  (this :
    limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
      ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
  LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
Tactic: rwa [this, _root_.sub_le_sub_iff_left ‖f‖] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have key : LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
  (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
Tactic: have key := h _ (f.add_norm_nonneg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
    (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have key₁ : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L ≤
  ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖
Tactic: simp_rw [f.integral_add_const ‖f‖] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L ≤
    ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have key₁ : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖
Tactic: simp only [probReal_univ, smul_eq_mul, one_mul] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have this : limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
  limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
Tactic: have := limsup_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖
this :
  limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
    limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have rwa : ∀ (key : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖ ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖)
  (this :
    limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
      limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
Tactic: rwa [this, add_le_add_iff_right] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖
this :
  limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
    limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
rwa :
  ∀
    (key :
      limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖ ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖)
    (this :
      limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
        limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
    LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have rwa₁ : ∀
  (key :
    LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
  (this :
    limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
      limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
Tactic: rwa [this, add_le_add_iff_right] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inl : ∀
  (h :
    ∀ (f : X →ᵇ ℝ),
      0 ≤ f →
        LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
          (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥)),
  Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥ (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
Tactic: rcases eq_or_neBot L with rfl | hL
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
inl :
  ∀
    (h :
      ∀ (f : X →ᵇ ℝ),
        0 ≤ f →
          LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
            (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥)),
    Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥ (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inr : ∀ (hL : L.NeBot),
  Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
Tactic: rcases eq_or_neBot L with rfl | hL
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
Tactic: have obs := BoundedContinuousFunction.isBounded_range_integral μs f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
Tactic: have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
Tactic: have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inr : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
Tactic: apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
inr : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inr₁ : LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
Tactic: apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
inr : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
inr₁ :
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inr₂ : autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
  tendsto_of_le_liminf_of_limsup_le._auto_1
Tactic: apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
inr : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
inr₁ :
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
inr₂ :
  autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_1
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inr₃ : autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
  tendsto_of_le_liminf_of_limsup_le._auto_3
Tactic: apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)