awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
calc_1 :
  ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop
calc_2 :
  ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
calc ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
      ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, atTop.liminf (fun i ↦ (μs i) {a | t < f a}) := ?_ -- (i)
    _ ≤ atTop.liminf (fun i ↦ ∫⁻ (t : ℝ) in Set.Ioi 0, (μs i) {a | t < f a}) := ?_

Premises used: Set.Ioi, Filter.liminf, setOf, MeasureTheory.Measure.restrict, Filter.atTop, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, DFunLike.coe, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
(lintegral_mono (fun t ↦ h_opens _ (continuous_def.mp f_cont _ isOpen_Ioi))).trans
            (le_refl _)

Premises used: le_refl, Set.Ioi, Set.Mem, setOf, isOpen_Ioi, Set.preimage, MeasureTheory.lintegral_mono, Iff.mp, LE.le.trans, continuous_def
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a} ≤
    ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
exact (lintegral_mono (fun t ↦ h_opens _ (continuous_def.mp f_cont _ isOpen_Ioi))).trans
            (le_refl _)

Premises used: le_refl, Set.Ioi, isOpen_Ioi, Set.preimage, MeasureTheory.lintegral_mono, Iff.mp, LE.le.trans, continuous_def
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
lintegral_liminf_le (fun n ↦ Antitone.measurable (fun s t hst ↦
            measure_mono (fun ω hω ↦ lt_of_le_of_lt hst hω)))

Premises used: lt_of_le_of_lt, Antitone.measurable, MeasureTheory.lintegral_liminf_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst_1, _] f
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i : (a : Set Ω) → ℝ≥0∞) {a : Ω | t < f a}) atTop

Tactic:
exact lintegral_liminf_le (fun n ↦ Antitone.measurable (fun s t hst ↦
            measure_mono (fun ω hω ↦ lt_of_le_of_lt hst hω)))

Premises used: lt_of_le_of_lt, Antitone.measurable, MeasureTheory.lintegral_liminf_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop

Tactic:
have same := lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
                  f.continuous f_nn h_opens
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
rw :
  (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μ).toReal ≤
    liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop
⊢ LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop)

Tactic:
rw [@integral_eq_lintegral_of_nonneg_ae Ω _ μ f (Eventually.of_forall f_nn)
        f.continuous.measurable.aestronglyMeasurable]

Premises used: Measurable.aestronglyMeasurable, Filter.Eventually.of_forall, BoundedContinuousFunction.continuous, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ (∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ).toReal ≤
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)

Tactic:
ENNReal.toReal_mono ?_ same

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
h :
  liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
convert! : Ne (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μ).toReal ≤
    liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop

Tactic:
convert! ENNReal.toReal_mono ?_ same

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
h :
  liminf (fun (i : ℕ) ↦ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μs i).toReal) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
⊢ liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)

Tactic:
simp only [fun i ↦ @integral_eq_lintegral_of_nonneg_ae Ω _ (μs i) f (Eventually.of_forall f_nn)
                        f.continuous.measurable.aestronglyMeasurable]

Premises used: Measurable.aestronglyMeasurable, Filter.Eventually.of_forall, BoundedContinuousFunction.continuous, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
i : ℕ
⊢ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑(nndist 0 g) : ℝ≥0∞)

Tactic:
simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using
            BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g

Premises used: ge_iff_le, MeasureTheory.IsProbabilityMeasure.measure_univ, coe_nnreal_ennreal_nndist, mul_one, BoundedContinuousFunction.lintegral_le_edist_mul
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
⊢ ∀ (i : ℕ), ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑(nndist 0 g) : ℝ≥0∞)

Tactic:
have bound : ∀ i, ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i) ≤ nndist 0 g := fun i ↦ by
      simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using
            BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
bound : ∀ (i : ℕ), ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑(nndist 0 g) : ℝ≥0∞)
⊢ liminf (fun (i : ℕ) ↦ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μs i).toReal) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)

Tactic:
apply ENNReal.liminf_toReal_eq ENNReal.coe_ne_top (Eventually.of_forall bound)

Premises used: ENNReal.liminf_toReal_eq, Filter.Eventually.of_forall, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
h : LT.lt (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
⊢ Ne (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ ∀ (i : ℕ),
    ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤
      HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
have obs := fun (i : ℕ) ↦ @BoundedContinuousFunction.lintegral_nnnorm_le Ω _ _ (μs i) ℝ _ f
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs :
  ∀ (i : ℕ),
    ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤
      HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)

Tactic:
simp only [measure_univ, mul_one] at obs

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
apply : liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞

Tactic:
apply lt_of_le_of_lt _ (show (‖f‖₊ : ℝ≥0∞) < ∞ from ENNReal.coe_lt_top)

Premises used: lt_of_le_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
hf :
  autoParam
    (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
      ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i)
    liminf_le_of_le._auto_1
h : ∀ (b : ℝ≥0∞), (∀ᶠ (n : ℕ) in atTop, b ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n) → b ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop ≤ (↑‖f‖₊ : ℝ≥0∞)

Tactic:
apply liminf_le_of_le

Premises used: Filter.liminf_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ ∀ (x : ℝ≥0∞), (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) x 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ autoParam
    (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
      ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i)
    liminf_le_of_le._auto_1

Tactic:
refine ⟨0, .of_forall (by simp)⟩
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
h : ∀ (i : ℕ) (hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i), x ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ x ≤ (↑‖f‖₊ : ℝ≥0∞)

Tactic:
obtain ⟨i, hi⟩ := hx.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
h : ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ x ≤ (↑‖f‖₊ : ℝ≥0∞)

Tactic:
apply le_trans hi

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
⊢ ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)

Tactic:
obs i