awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have mpr : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2 ≤ (↑μ : Measure Ω).real s + ε
Tactic: apply (Filter.limsup_le_of_le ?_ ev_near).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 + ε
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have apply : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) F fun (n : γ) ↦ (↑(μs n) : Measure Ω).real s
Tactic: apply (Filter.limsup_le_of_le ?_ ev_near).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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
⊢ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2 ≤ (↑μ : Measure Ω).real s + ε
have mpr : (↑μ : Measure Ω).real s + ε / 2 + ε / 2 = (↑μ : Measure Ω).real s + ε
Tactic: apply (add_le_add (hM M rfl.le).le (le_refl (ε / 2))).trans_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (fun (i : ι) ↦ (μ i).real (⋃ s ∈ t, s)) l (𝓝 (ν.real (⋃ s ∈ t, s)))
have A : ∀ (i : ι),
  (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
Tactic: have A (i) : (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty,
      (-1 : ℝ) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s) :=
    measureReal_biUnion_eq_sum_powerset (fun s hs ↦ hmeas _ (ht _ hs))
      (fun s hs ↦ hμ _ (ht _ hs) i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
⊢ Tendsto (fun (i : ι) ↦ (μ i).real (⋃ s ∈ t, s)) l (𝓝 (ν.real (⋃ s ∈ t, s)))
have simp_rw : Tendsto (β := ℝ)
  (fun (i : ι) ↦ ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
  (𝓝 (∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * ν.real (⋂ i ∈ u, i)))
Tactic: simp_rw [A, measureReal_biUnion_eq_sum_powerset (fun s hs ↦ hmeas _ (ht _ hs))
    (fun s hs ↦ hν _ (ht _ hs))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
⊢ Tendsto (β := ℝ)
    (fun (i : ι) ↦ ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
    (𝓝 (∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * ν.real (⋂ i ∈ u, i)))
have refine : ∀ (u : Finset (Set Ω)) (hu : u ∈ {u ∈ t.powerset | u.Nonempty}),
  Tendsto (fun (i : ι) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
    (𝓝 (HPow.hPow (α := ℝ) (-1) (#u + 1) * ν.real (⋂ i ∈ u, i)))
Tactic: refine tendsto_finsetSum _ (fun u hu ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ∈ {u ∈ t.powerset | u.Nonempty}
⊢ Tendsto (fun (i : ι) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
    (𝓝 (HPow.hPow (α := ℝ) (-1) (#u + 1) * ν.real (⋂ i ∈ u, i)))
have hu₁ : u ⊆ t ∧ u.Nonempty
Tactic: simp only [Finset.mem_filter, Finset.mem_powerset] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
⊢ Tendsto (fun (i : ι) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
    (𝓝 (HPow.hPow (α := ℝ) (-1) (#u + 1) * ν.real (⋂ i ∈ u, i)))
have hf : Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
Tactic: apply Filter.Tendsto.const_mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
⊢ Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
have hf : ∀ (h'u : Eq.{u_1 + 1} (α := Set Ω) (⋂ s ∈ u, s) ∅),
  Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
Tactic: rcases eq_empty_or_nonempty (⋂ s ∈ u, s) with h'u | h'u
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
hf :
  ∀ (h'u : Eq.{u_1 + 1} (α := Set Ω) (⋂ s ∈ u, s) ∅),
    Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
⊢ Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
have hf₁ : ∀ (h'u : Set.Nonempty.{u_1} (α := Ω) (⋂ s ∈ u, s)),
  Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
Tactic: rcases eq_empty_or_nonempty (⋂ s ∈ u, s) with h'u | h'u
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ : ∀ s ∈ S, ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ i : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (i : ι),
    (μ i).real (⋃ s ∈ t, s) =
      ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
h'u : Set.Nonempty.{u_1} (α := Ω) (⋂ s ∈ u, s)
⊢ Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
have hf : ⋂ s ∈ u, s ∈ S
Tactic: apply h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
⊢ Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν : Measure Ω).real (⋃ s ∈ t, s)))
have apply : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real s) l (𝓝 ((↑ν : Measure Ω).real s))
Tactic: apply hS.tendsto_measureReal_biUnion ht hmeas
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) (⋃ s ∈ t, s) : ℝ≥0)) l
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ s ∈ t, s)) : Filter ℝ≥0)
have this : Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν : Measure Ω).real (⋃ s ∈ t, s)))
Tactic: have : Tendsto (fun i ↦ (μ i : Measure Ω).real (⋃ s ∈ t, s)) l
      (𝓝 ((ν : Measure Ω).real (⋃ s ∈ t, s))) := by
    apply hS.tendsto_measureReal_biUnion ht hmeas
    simpa using h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
have this : ∀ (x : (↑G : Type u_1)), ∃ s ∈ S, s ∈ 𝓝 (↑x : Ω) ∧ s ⊆ G
Tactic: have : ∀ (x : G), ∃ s ∈ S, s ∈ 𝓝 (x : Ω) ∧ s ⊆ G := fun x ↦ h G hG x x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
this : ∀ (x : (↑G : Type u_1)), ∃ s ∈ S, s ∈ 𝓝 (↑x : Ω) ∧ s ⊆ G
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
have choose! : ∀ (s : (x : (↑G : Type u_1)) → Set Ω) (hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S)
  (hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)) (hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G),
  ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
Tactic: choose! s hsS hs_nhds hsG using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
have rcases : ∀ (T₀ : Set (↑G : Type u_1)) (T₀_count : T₀.Countable)
  (hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))),
  ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
Tactic: rcases TopologicalSpace.isOpen_iUnion_countable (fun i ↦ interior (s i))
      (fun i ↦ isOpen_interior) with ⟨T₀, T₀_count, hT₀⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
have refine : ⋃ t ∈ s '' T₀, t = G
Tactic: refine ⟨s '' T₀, by grind, T₀_count.image s, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
⊢ ⋃ t ∈ s '' T₀, t ⊆ G
have simp : ∀ (i : Set Ω) (i_1 : Ω) (i_2 : i_1 ∈ G),
  Subtype.mk (p := fun (a : Ω) ↦ a ∈ G) i_1 i_2 ∈ T₀ → s (Subtype.mk (p := fun (a : Ω) ↦ a ∈ G) i_1 i_2) = i → i ⊆ G
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
⊢ ⋃ t ∈ s '' T₀, t = G
have refine : G ⊆ ⋃ t ∈ s '' T₀, t
Tactic: refine Subset.antisymm (by simp; grind) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
⊢ G ⊆ ⋃ t ∈ s '' T₀, t
have this : G ⊆ ⋃ (i : (↑G : Type u_1)), interior (s i)
Tactic: have : G ⊆ ⋃ i, interior (s i) := by
      intro y hy
      simpa using ⟨y, hy, mem_interior_iff_mem_nhds.2 (hs_nhds ⟨y, hy⟩)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
this : G ⊆ ⋃ (i : (↑G : Type u_1)), interior (s i)
⊢ G ⊆ ⋃ t ∈ s '' T₀, t
have apply : Subset.{u_1} (α := Set Ω) (⋃ (i : (↑G : Type u_1)), interior (s i)) (⋃ t ∈ s '' T₀, t)
Tactic: apply this.trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
this : G ⊆ ⋃ (i : (↑G : Type u_1)), interior (s i)
⊢ Subset.{u_1} (α := Set Ω) (⋃ (i : (↑G : Type u_1)), interior (s i)) (⋃ t ∈ s '' T₀, t)
have rw : Subset.{u_1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ y ∈ T₀, s y)
Tactic: rw [← hT₀, biUnion_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have obtain : ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G),
  ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
Tactic: obtain ⟨T, TS, T_count, hT⟩ : ∃ T : Set (Set Ω), T ⊆ S ∧ T.Countable ∧ ⋃ t ∈ T, t = G := by
    have : ∀ (x : G), ∃ s ∈ S, s ∈ 𝓝 (x : Ω) ∧ s ⊆ G := fun x ↦ h G hG x x.2
    choose! s hsS hs_nhds hsG using this
    rcases TopologicalSpace.isOpen_iUnion_countable (fun i ↦ interior (s i))
      (fun i ↦ isOpen_interior) with ⟨T₀, T₀_count, hT₀⟩
    refine ⟨s '' T₀, by grind, T₀_count.image s, ?_⟩
    refine Subset.antisymm (by simp; grind) ?_
    have : G ⊆ ⋃ i, interior (s i) := by
      intro y hy
      simpa using ⟨y, hy, mem_interior_iff_mem_nhds.2 (hs_nhds ⟨y, hy⟩)⟩
    apply this.trans
    rw [← hT₀, biUnion_image]
    exact iUnion₂_mono fun i j ↦ interior_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
⊢ T.Nonempty
have contrapose! : ∀ (hr : T = ∅), (ν : (a : Set Ω) → ℝ≥0) G ≤ r
Tactic: contrapose! hr
Cleared hypotheses: hr