mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ✝ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ✝)
n : ℕ
h : Monotone K
this✝² : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝¹ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this✝ :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ μ (K m \ K n) ≤ u n

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ✝ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ✝)
n : ℕ
h : Monotone K
this✝² : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝¹ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this✝ :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ μ (K m \ K n) ≤ u n
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ IsFiniteMeasure ((μ.withDensity g).restrict tᶜ)

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ IsFiniteMeasure ((μ.withDensity g).restrict tᶜ)
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
⊢ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g ≤
    (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g

pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
⊢ g ≤ᵐ[μ.restrict tᶜ] f

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
⊢ g ≤ᵐ[μ.restrict tᶜ] f
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
this : {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} = {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C}
⊢ IsCompact ({μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C})

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
this : {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} = {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C}
⊢ IsCompact ({μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C})
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f ≤ μ.withDensity (f - g + g)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f ≤ μ.withDensity (f - g + g)
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose) = ae μ

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose) = ae μ
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure (if IsFiniteMeasure μ then μ else ⋯.choose)

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure (if IsFiniteMeasure μ then μ else ⋯.choose)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
t : Set α
left✝ : s ⊆ t
mt : MeasurableSet t
ht : μ t = μ s
⊢ μ t = 0 ∨ μ t = 1

Tactic:
]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
t : Set α
left✝ : s ⊆ t
mt : MeasurableSet t
ht : μ t = μ s
⊢ μ t = 0 ∨ μ t = 1
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ = μ

pp: case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
]

Goal state after:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ IsFiniteMeasure μ
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure μ.toFiniteAux[|univ]

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure μ.toFiniteAux[|univ]
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case mp.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
h : μ s = 1
h₀ : μ univ = 0
this : 1 ≤ μ univ
⊢ μ univ = 1

Tactic:
]

Goal state after:
case mp.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
h : μ s = 1
h₀ : μ univ = 0
this : 1 ≤ μ univ
⊢ μ univ = 1
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ∞ • μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ = ∞ • μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ∞ • μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ = ∞ • μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ ∞ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ∞ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ ∞ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ∞ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ∞ * 0 = ∞ * 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ∞ = ∞

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) ≠ 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) ≠ 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
this : 1 - μ (s ∩ t) ≤ 0
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
this : 1 - μ (s ∩ t) ≤ 0
⊢ False
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
this :
  ProbabilityMeasure.toFiniteMeasure '' {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} = {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
⊢ IsCompact {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
this :
  ProbabilityMeasure.toFiniteMeasure '' {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} = {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
⊢ IsCompact {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ 0 + 0 ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ 0 + 0 ≤ 0
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ ε / 2 * ((↑N + 1) * (1 / (↑N + 1))) ≤ ε / 2

Tactic:
]

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ ε / 2 * ((↑N + 1) * (1 / (↑N + 1))) ≤ ε / 2
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

pp: case hf
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∀ (i : ℕ), (⇑μ ∘ fun n ↦ T n ∩ s) i ≠ ∞

pp: case hx
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ μ (⋃ n, T n ∩ s) ≠ ∞

Tactic:
]

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

case hf
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∀ (i : ℕ), (⇑μ ∘ fun n ↦ T n ∩ s) i ≠ ∞

case hx
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ μ (⋃ n, T n ∩ s) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
n : ℕ
h : ¬μ (A n) = 1
⊢ μ (A n) = 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
n : ℕ
h : ¬μ (A n) = 1
⊢ μ (A n) = 0
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases (Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite
        (μ.restrict (T N)) h𝒜 hgen).approx s ms
        (ne_of_lt (lt_of_le_of_lt (μ.restrict_apply_le _ s) hμs.lt_top))
        (ε / 2) (by linarith [ε_pos])
        with ⟨t, t_mem, ht⟩

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ ∅ = 1
h : ⋂ n, B n = ∅
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ ∅ = 1
h : ⋂ n, B n = ∅
⊢ False
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ μ (s ∆ (t ∩ T N)) ≤ μ (s ∆ (s ∩ T N)) + μ ((s ∩ T N) ∆ (t ∩ T N))

Tactic:
]

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ μ (s ∆ (t ∩ T N)) ≤ μ (s ∆ (s ∩ T N)) + μ ((s ∩ T N) ∆ (t ∩ T N))