awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : TopologicalSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst_2 : L.IsCountablyGenerated
h : ∀ (F : Set Ω), IsClosed[inst] F → limsup (fun (i : ι) ↦ (↑(μs i) : Measure Ω).real F) L ≤ (↑μ : Measure Ω).real F
⊢ ∀ (F : Set Ω),
    IsClosed[inst] F →
      LE.le (α := ℝ≥0) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0) F) L : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) F : ℝ≥0)

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 Ω
mp :
  Tendsto μs F (𝓝 μ) →
    ∀ (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 Ω)))
mpr :
  (∀ (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 Ω)))) →
    Tendsto μs F (𝓝 μ)
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (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 Ω)))

Tactic:
constructor
-- 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 Ω
h : Tendsto μs F (𝓝 μ)
f : Ω → ℝ
hf_bounded : ∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C
hf_lip : ∃ (L : ℝ≥0), LipschitzWith L f
⊢ ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))

Tactic:
simp_rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto] at h

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
-- 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 Ω
f : Ω → ℝ
hf_bounded : ∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C
hf_lip : ∃ (L : ℝ≥0), LipschitzWith L f
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))
f' : Ω →ᵇ ℝ := { toFun := f, continuous_toFun := ⋯, map_bounded' := hf_bounded }
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))

Tactic:
simpa using h f'
-- 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 Ω
mpr :
  ∀ [IsCountablyGenerated.{u_1} (α := γ) ⊥],
    (∀ (f : Ω → ℝ),
        (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
          (∃ (L : ℝ≥0), LipschitzWith L f) →
            Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) ⊥
              (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
      Tendsto μs ⊥ (𝓝 μ)
mpr₁ :
  ∀ (hne : F.NeBot),
    (∀ (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 Ω)))) →
      Tendsto μs F (𝓝 μ)
⊢ (∀ (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 Ω)))) →
    Tendsto μs F (𝓝 μ)

Tactic:
rcases F.eq_or_neBot with rfl | hne

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
inst_2 : IsCountablyGenerated.{u_1} (α := γ) ⊥
⊢ (∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) ⊥
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
    Tendsto μs ⊥ (𝓝 μ)

Tactic:
simp
-- 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
⊢ (∀ (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 Ω)))) →
    Tendsto μs F (𝓝 μ)

Tactic:
fun h ↦ tendsto_of_forall_isClosed_limsup_real_le' fun s hs ↦ ?_

Premises used: MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le'
-- 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
mpr :
  ∀
    (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),
    limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s
⊢ (∀ (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 Ω)))) →
    Tendsto μs F (𝓝 μ)

Tactic:
refine fun h ↦ tendsto_of_forall_isClosed_limsup_real_le' fun s hs ↦ ?_

Premises used: MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le'
-- 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
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s

Tactic:
le_of_forall_pos_le_add fun ε ε_pos ↦ ?_

Premises used: le_of_forall_pos_le_add
-- 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
mpr : ∀ (ε : ℝ) (ε_pos : 0 < ε), limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s

Tactic:
refine le_of_forall_pos_le_add fun ε ε_pos ↦ ?_

Premises used: le_of_forall_pos_le_add
-- 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 < ε
n : ℕ
ω : Ω
⊢ 0 < 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 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) ω) : ℝ)
x : ℕ
⊢ LT.lt (α := ℝ) 0 ((fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) x)

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) ω) : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))

Tactic:
have key₁ : Tendsto (fun n ↦ ∫ ω, fs n ω ∂μ) atTop (𝓝 ((μ : Measure Ω).real s)) :=
    tendsto_integral_thickenedIndicator_of_isClosed μ hs (δs := fun n ↦ (1 : ℝ) / (n + 1))
      (fun _ ↦ by positivity) tendsto_one_div_add_atTop_nhds_zero_nat
-- 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))
⊢ (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2

Tactic:
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))
⊢ (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2

Tactic:
have room₁ : (μ : Measure Ω).real s < (μ : Measure Ω).real s + ε / 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
mpr :
  ∀ (M : ℕ) (hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2),
    limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε

Tactic:
obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁

Premises used: Filter.Tendsto.eventually_lt_const, Iff.mp, Filter.eventually_atTop
-- 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
⊢ 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
mpr :
  ∀
    (key₂ :
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))),
    limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
mpr₁ : ∀ (x y : Ω), dist (fs M x) (fs M y) ≤ 1
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε

Tactic:
have key₂ : Tendsto (fun i ↦ ∫ ω, fs M ω ∂(μs i)) F (𝓝 (∫ ω, fs M ω ∂μ)) :=
    h (fs M) ⟨1, fun x y ↦ ?_⟩
      ⟨_, lipschitzWith_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 :
  ∀ (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
x y : Ω
mpr : -1 ≤ fs M x - fs M y ∧ fs M x - fs M y ≤ 1
⊢ dist (fs M x) (fs M y) ≤ 1

Tactic:
simp only [Real.dist_eq, abs_le]

Premises used: abs_le, Real.dist_eq
-- 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
x y : Ω
⊢ ∀ (x : Ω), fs M x ≤ 1

Tactic:
have h1 x : fs M x ≤ 1 := thickenedIndicator_le_one _ _ _
-- 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
x_1 y : Ω
h1 : ∀ (x : Ω), fs M x ≤ 1
x : Ω
⊢ 0 ≤ fs M x

Tactic:
simp [fs]
-- 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
x y : Ω
h1 : ∀ (x : Ω), fs M x ≤ 1
⊢ ∀ (x : Ω), 0 ≤ fs M x

Tactic:
have h2 x : 0 ≤ fs M x := by simp [fs]
-- 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
x y : Ω
h1 : ∀ (x : Ω), fs M x ≤ 1
h2 : ∀ (x : Ω), 0 ≤ fs M x
⊢ -1 ≤ fs M x - fs M y ∧ fs M x - fs M y ≤ 1

Tactic:
grind
-- 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:
simp [ε_pos]