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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := ⟨↑μ, ⋯⟩
s✝ : Set E
a✝ : MeasurableSet s✝
⊢ ↑ν.toFiniteMeasure s✝ = ↑μ s✝

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
μ : FiniteMeasure E
hμ : μ.mass = 1
h'μ : ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
ν : ProbabilityMeasure E := ⟨↑μ, ⋯⟩
s✝ : Set E
a✝ : MeasurableSet s✝
⊢ ↑ν.toFiniteMeasure s✝ = ↑μ s✝
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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
⊢ 0 < u n

Tactic:
;

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
⊢ 0 < u n
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
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
have : Fact (μ (T N) < ∞) := Fact.mk <| T_finite N

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 ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε
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 ∩ T N) ∆ s) + μ (s ∆ t ∩ T N)

Tactic:
symmDiff_comm _ s,

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 ∩ T N)
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp (fun x ↦ f x i) p μ
x✝¹ : X
x✝ : ι
⊢ f x✝¹ x✝ = (∑ i, Pi.single i ∘ fun x ↦ f x i) x✝¹ x✝

Tactic:
;

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp (fun x ↦ f x i) p μ
x✝¹ : X
x✝ : ι
⊢ f x✝¹ x✝ = (∑ i, Pi.single i ∘ fun x ↦ f x i) x✝¹ x✝
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
⊢ MemLp f 1 μ ↔ ∀ (i : ι), MemLp (fun x ↦ f x i) 1 μ

Tactic:
memLp_pi_iff

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

Goal state before:
pp: case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop, (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
;

Goal state after:
case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop, (fun x1 x2 ↦ x1 ≥ x2) x 0
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: case fst
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
x✝ : X
⊢ (f x✝).1 = (((⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2) x✝).1

pp: case snd
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
x✝ : X
⊢ (f x✝).2 = (((⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2) x✝).2

Tactic:
;

Goal state after:
case fst
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
x✝ : X
⊢ (f x✝).1 = (((⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2) x✝).1

case snd
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
x✝ : X
⊢ (f x✝).2 = (((⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2) x✝).2
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp

Tactic:
;

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp

Tactic:
;

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ sub k), U i))) atTop, (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
;

Goal state after:
case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ sub k), U i))) atTop, (fun x1 x2 ↦ x1 ≥ x2) x 0
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ ↑((μ (sub b_1)) (⋃ i, ⋃ (_ : i ≤ sub b_1), U i))
⊢ ε ≤ 1

Tactic:
;

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ ↑((μ (sub b_1)) (⋃ i, ⋃ (_ : i ≤ sub b_1), U i))
⊢ ε ≤ 1
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case refine_2.refine_1
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ‖indicatorConstLp p ms ⋯ a - indicatorConstLp p ms hμs b‖ ≤ ε / 3

Tactic:
rw [indicatorConstLp_sub, norm_indicatorConstLp p_ne_zero p_ne_top.elim]

Goal state after:
case refine_2.refine_1
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ‖a - b‖ * μ.real s ^ (1 / p.toReal) ≤ ε / 3
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ε / 3 * (μ.real s ^ (1 / p.toReal) / (1 + μ.real s ^ (1 / p.toReal))) ≤ ε / 3 * 1

Tactic:
exact mul_le_mul_of_nonneg_left
              ((div_le_one (by linarith [μs_pow_nonneg])).2 (by linarith))
              (by linarith [ε_pos])

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

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
Measurebound : ∀ (n : ℕ), ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ 1 - ε
accumulation : Tendsto (fun a ↦ ↑(μlim (⋃ i, ⋃ (_ : i ≤ a), U i))) atTop (𝓝 ↑1)
⊢ 0 < ε

Tactic:
;

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
Measurebound : ∀ (n : ℕ), ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ 1 - ε
accumulation : Tendsto (fun a ↦ ↑(μlim (⋃ i, ⋃ (_ : i ≤ a), U i))) atTop (𝓝 ↑1)
⊢ 0 < ε
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
⊢ ∑ p ∈ P, ‖μ p‖ₑ ≤ μ.variation s

Tactic:
set Q' := Q.ofSubset (filter_subset MeasurableSet Q.parts) rfl with defQ'

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
⊢ ∑ p ∈ P, ‖μ p‖ₑ ≤ μ.variation s
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
⊢ ∀ (t : Set X), ¬t = ∅ → t ∈ P → MeasurableSet t → t ⊆ s

Tactic:
;

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
⊢ ∀ (t : Set X), ¬t = ∅ → t ∈ P → MeasurableSet t → t ⊆ s