awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
⊢ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2

Tactic:
have room₂ : ∫ a, fs M a ∂μ < ∫ a, fs M a ∂μ + ε / 2 := by simp [ε_pos]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2

Tactic:
(key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx

Premises used: Filter.Tendsto.eventually_le_const, Filter.Eventually.mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
refine :
  ∀ (x : γ) (hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2),
    (↑(μs x) : Measure Ω).real s ≤ ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω)
⊢ ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2

Tactic:
refine (key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx

Premises used: Filter.Tendsto.eventually_le_const, Filter.Eventually.mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
rw : LE.le (α := ℝ) (∫ (x : Ω), s.indicator 1 x ∂(↑(μs x) : Measure Ω)) (∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω))
⊢ (↑(μs x) : Measure Ω).real s ≤ ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω)

Tactic:
rw [← integral_indicator_one hs.measurableSet]

Premises used: MeasureTheory.integral_indicator_one, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ LE.le (α := ℝ) (∫ (x : Ω), s.indicator 1 x ∂(↑(μs x) : Measure Ω)) (∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω))

Tactic:
integral_mono ?_ (integrable_thickenedIndicator _ _) ?_

Premises used: MeasureTheory.integral_mono, MeasureTheory.integrable_thickenedIndicator
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
refine_1 : Integrable (ε := ℝ) (s.indicator 1) (↑(μs x) : Measure Ω)
refine_2 : s.indicator 1 ≤ fs M
⊢ LE.le (α := ℝ) (∫ (x : Ω), s.indicator 1 x ∂(↑(μs x) : Measure Ω)) (∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω))

Tactic:
refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_

Premises used: MeasureTheory.integral_mono, MeasureTheory.integrable_thickenedIndicator
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ Integrable (ε := ℝ) (s.indicator 1) (↑(μs x) : Measure Ω)

Tactic:
(integrable_indicator_iff hs.measurableSet).mpr (integrable_const _).integrableOn

Premises used: Iff.mpr, IsClosed.measurableSet, MeasureTheory.Integrable.integrableOn, MeasureTheory.integrable_const, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ Integrable (ε := ℝ) (s.indicator 1) (↑(μs x) : Measure Ω)

Tactic:
exact (integrable_indicator_iff hs.measurableSet).mpr (integrable_const _).integrableOn

Premises used: Iff.mpr, IsClosed.measurableSet, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ 0 < 1 / HAdd.hAdd (α := ℝ) (↑M : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ (fun (i : Ω) ↦ (↑(s.indicator (fun (x : Ω) ↦ 1) i) : ℝ)) ≤ fs M

Tactic:
have h : _ ≤ fs M :=
        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h_1 :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
h : (fun (i : Ω) ↦ (↑(s.indicator (fun (x : Ω) ↦ 1) i) : ℝ)) ≤ fs M
⊢ s.indicator 1 ≤ fs M

Tactic:
simpa using h
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2

Tactic:
have ev_near : ∀ᶠ x in F, (μs x : Measure Ω).real s ≤ ∫ a, fs M a ∂μ + ε / 2 := by
    refine (key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx
    rw [← integral_indicator_one hs.measurableSet]
    refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_
    · exact (integrable_indicator_iff hs.measurableSet).mpr (integrable_const _).integrableOn
    · have h : _ ≤ fs M :=
        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
      simpa using h
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
ev_near : ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
mpr : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2 ≤ (↑μ : Measure Ω).real s + ε
apply : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) F fun (n : γ) ↦ (↑(μs n) : Measure Ω).real s
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε

Tactic:
apply (Filter.limsup_le_of_le ?_ ev_near).trans

Premises used: Filter.limsup_le_of_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
ev_near : ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
mpr : (↑μ : Measure Ω).real s + ε / 2 + ε / 2 = (↑μ : Measure Ω).real s + ε
⊢ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2 ≤ (↑μ : Measure Ω).real s + ε

Tactic:
apply (add_le_add (hM M rfl.le).le (le_refl (ε / 2))).trans_eq

Premises used: le_refl, LE.le.trans_eq, add_le_add, HDiv.hDiv, LT.lt.le, Eq.le, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
ev_near : ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ (↑μ : Measure Ω).real s + ε / 2 + ε / 2 = (↑μ : Measure Ω).real s + ε

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
ev_near : ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ ∀ (i : γ), 0 ≤ (↑(μs i) : Measure Ω).real s

Tactic:
simp