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 Ω)))
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
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) F fun (n : γ) ↦ (↑(μs n) : Measure Ω).real s

Tactic:
exact isCoboundedUnder_le_of_le F (x := 0) (by simp)

Premises used: Filter.isCoboundedUnder_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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∞)
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
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)))
⊢ Tendsto (fun (i : ι) ↦ (μ i).real (⋃ s ∈ t, s)) l (𝓝 (ν.real (⋃ s ∈ t, s)))

Tactic:
simp_rw [A, measureReal_biUnion_eq_sum_powerset (fun s hs ↦ hmeas _ (ht _ hs))
    (fun s hs ↦ hν _ (ht _ hs))]

Premises used: MeasureTheory.measureReal_biUnion_eq_sum_powerset
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)))

Tactic:
tendsto_finsetSum _ (fun u hu ↦ ?_)

Premises used: tendsto_finsetSum
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
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)))
⊢ 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:
refine tendsto_finsetSum _ (fun u hu ↦ ?_)

Premises used: tendsto_finsetSum
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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}
⊢ u ⊆ t ∧ u.Nonempty

Tactic:
simp only [Finset.mem_filter, Finset.mem_powerset] at hu

Premises used: Finset.mem_powerset, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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 : Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))
⊢ Tendsto (fun (i : ι) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
    (𝓝 (HPow.hPow (α := ℝ) (-1) (#u + 1) * ν.real (⋂ i ∈ u, i)))

Tactic:
apply Filter.Tendsto.const_mul

Premises used: Filter.Tendsto.const_mul
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)))
hf₁ :
  ∀ (h'u : Set.Nonempty.{u_1} (α := Ω) (⋂ 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)))

Tactic:
rcases eq_empty_or_nonempty (⋂ s ∈ u, s) with h'u | h'u

Premises used: Set.iInter, Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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 : Eq.{u_1 + 1} (α := Set Ω) (⋂ s ∈ u, s) ∅
⊢ Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))

Tactic:
simpa [h'u] using tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
hf : ⋂ s ∈ u, s ∈ S
⊢ Tendsto (fun (x : ι) ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))

Tactic:
apply h
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ⋂ s ∈ u, s ∈ S

Tactic:
hS.biInter_mem hu.2 (fun s hs ↦ ht _ (hu.1 hs)) h'u

Premises used: IsPiSystem.biInter_mem, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ⋂ s ∈ u, s ∈ S

Tactic:
exact hS.biInter_mem hu.2 (fun s hs ↦ ht _ (hu.1 hs)) h'u

Premises used: IsPiSystem.biInter_mem, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
apply : ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real s) l (𝓝 ((↑ν : Measure Ω).real s))
⊢ Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν : Measure Ω).real (⋃ s ∈ t, s)))

Tactic:
apply hS.tendsto_measureReal_biUnion ht hmeas

Premises used: IsPiSystem.tendsto_measureReal_biUnion
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
⊢ ∀ s ∈ S, Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real s) l (𝓝 ((↑ν : Measure Ω).real s))

Tactic:
simpa using h
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)))

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
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
this : Tendsto (fun (i : ι) ↦ (↑(μ i) : Measure Ω).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν : Measure Ω).real (⋃ s ∈ t, s)))
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) (⋃ s ∈ t, s) : ℝ≥0)) l
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ s ∈ t, s)) : Filter ℝ≥0)

Tactic:
simpa using this
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G

Tactic:
choose! s hsS hs_nhds hsG using this
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
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
⊢ ∃ 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₀⟩

Premises used: TopologicalSpace.isOpen_iUnion_countable, isOpen_interior, interior
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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))
⊢ s '' T₀ ⊆ S

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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))
refine : ⋃ t ∈ s '' T₀, t = G
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G

Tactic:
refine ⟨s '' T₀, by grind, T₀_count.image s, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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))
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
⊢ ⋃ t ∈ s '' T₀, t ⊆ G

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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))
⊢ ∀ (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:
grind
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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))
refine : G ⊆ ⋃ t ∈ s '' T₀, t
⊢ ⋃ t ∈ s '' T₀, t = G

Tactic:
refine Subset.antisymm (by simp; grind) ?_

Premises used: Set.Subset.antisymm
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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))
y : Ω
hy : y ∈ G
⊢ Membership.mem (γ := Set Ω) (⋃ (i : (↑G : Type u_1)), interior (s i)) y

Tactic:
simpa using ⟨y, hy, mem_interior_iff_mem_nhds.2 (hs_nhds ⟨y, hy⟩)⟩
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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 ⊆ ⋃ (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⟩)⟩
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
apply : Subset.{u_1} (α := Set Ω) (⋃ (i : (↑G : Type u_1)), interior (s i)) (⋃ t ∈ s '' T₀, t)
⊢ G ⊆ ⋃ t ∈ s '' T₀, t

Tactic:
apply this.trans

Premises used: HasSubset.Subset.trans