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

Goal state before:
pp: α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ∫ (t : ℝ) in Ioc 0 ‖f‖, μ.real {a | t ≤ f a} = ∫ (t : ℝ) in Ioc 0 ‖f‖, μ.real {a | t ≤ f a}

pp: α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ Integrable (⇑f) μ

pp: α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ⇑f ≤ᵐ[μ] fun x ↦ ‖f‖

Tactic:
]

Goal state after:
α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ Integrable (⇑f) μ

α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ⇑f ≤ᵐ[μ] fun x ↦ ‖f‖
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
⊢ ∫ (t : ℝ) in Ioc 0 ‖f‖, μ.real {a | t ≤ f a} ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
⊢ ∫ (t : ℝ) in Ioc 0 ‖f‖, μ.real {a | t ≤ f a} ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ (ν (thickening ε {a | t ≤ f a})).toReal + ε = (ν (thickening ε {a | t ≤ f a})).toReal + ε

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ ball x ε ⊆ u

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ ball x ε ⊆ u
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ * ↑ν univ).toNNReal

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ * ↑ν univ).toNNReal
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
ν : FiniteMeasure β
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Measure.map (Prod.map f g) ((↑μ).prod ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Measure.map (Prod.map f g) ((↑μ).prod ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Tactic:
]

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

Goal state before:
pp: case hg
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ε) (volume.restrict (Ioc 0 ‖f‖))

Tactic:
· exact integrable_const ε

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
a : Set α
b : Set β
ameas : MeasurableSet a
ha : ↑μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : ↑μ.1 (frontier a') = 0
b'meas : MeasurableSet b'
hb' : μ.2 (frontier b') = 0
⊢ ↑μ.1 (frontier (a ∩ a')) = 0

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
a : Set α
b : Set β
ameas : MeasurableSet a
ha : ↑μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : ↑μ.1 (frontier a') = 0
b'meas : MeasurableSet b'
hb' : μ.2 (frontier b') = 0
⊢ ↑μ.1 (frontier (a ∩ a')) = 0
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : ↑μ.2 (frontier b) = 0
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : μ.1 (frontier a') = 0
b'meas : MeasurableSet b'
hb' : ↑μ.2 (frontier b') = 0
⊢ ↑μ.2 (frontier (b ∩ b')) = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : ↑μ.2 (frontier b) = 0
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : μ.1 (frontier a') = 0
b'meas : MeasurableSet b'
hb' : ↑μ.2 (frontier b') = 0
⊢ ↑μ.2 (frontier (b ∩ b')) = 0
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
⊢ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(Ps i)) atTop (𝓝 (∫ (ω : Ω), f ω ∂↑P))

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
⊢ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(Ps i)) atTop (𝓝 (∫ (ω : Ω), f ω ∂↑P))
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, dist (μs n) ν + εs n ∈ Ioi 0

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, dist (μs n) ν + εs n ∈ Ioi 0
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ 0 < dist (μs n) ν + εs n

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ 0 < dist (μs n) ν + εs n
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
have ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0) := by
      rw [tendsto_nhdsWithin_iff]
      refine ⟨by simpa using ε_of_room, Eventually.of_forall fun n ↦ ?_⟩
      · rw [mem_Ioi]
        linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)]

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
]

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball (x.1, x.2) ε ⊆ u

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball (x.1, x.2) ε ⊆ u
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case refine_1
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
⊢ ν' (Subtype.val ⁻¹' Kᶜ) = 0

Tactic:
]

Goal state after:
case refine_1
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
⊢ ν' (Subtype.val ⁻¹' Kᶜ) = 0
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case e'_2
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂μ = ∫ (y : X), g y ∂Measure.map Subtype.val μ'

Tactic:
]

Goal state after:
case e'_2
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂μ = ∫ (y : X), g y ∂Measure.map Subtype.val μ'
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case e'_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : { x // x ∈ K }), g ↑x ∂ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'

Tactic:
]

Goal state after:
case e'_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : { x // x ∈ K }), g ↑x ∂ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ ((DomMulAct.mk g' * DomMulAct.mk g) • addHaar).addHaarScalarFactor (DomMulAct.mk g' • addHaar) *
      (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar

Tactic:
]

Goal state after:
G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ ((DomMulAct.mk g' * DomMulAct.mk g) • addHaar).addHaarScalarFactor (DomMulAct.mk g' • addHaar) *
      (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: case e_a
G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar = (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar

Tactic:
]

Goal state after: