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

Goal state before:
pp: case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ μ.real {x | r < |⟪a, x⟫|} = μ.real ((fun x ↦ ⟪a, x⟫) ⁻¹' {x | r < |x|})

pp: case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ MeasurableSet {x | r < |x|}

Tactic:
]

Goal state after:
case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ μ.real {x | r < |⟪a, x⟫|} = μ.real ((fun x ↦ ⟪a, x⟫) ⁻¹' {x | r < |x|})

case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ MeasurableSet {x | r < |x|}
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : BorelSpace E
inst✝³ : T2Space E
inst✝² : ContinuousSMul ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this : NormedAddCommGroup F := p.toNormedAddCommGroup
⊢ μ {x | g x ≤ r} = μ {x | g x < r}

Tactic:
let : NormedSpace ℝ F := { norm_smul_le := fun _ _ ↦ h5 _ _ }

Goal state after:
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : BorelSpace E
inst✝³ : T2Space E
inst✝² : ContinuousSMul ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝ : NormedAddCommGroup F := p.toNormedAddCommGroup
this : NormedSpace ℝ F := { toModule := inst✝⁷, norm_smul_le := ⋯ }
⊢ μ {x | g x ≤ r} = μ {x | g x < r}
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case e'_4
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
x : ℝ
⊢ ∫ (x_1 : E), cexp (↑x * ↑⟪x_1, a⟫ * I) ∂μ = ∫ (x_1 : E), cexp (↑x * ↑⟪a, x_1⟫ * I) ∂μ

Tactic:
]

Goal state after:
case e'_4
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
x : ℝ
⊢ ∫ (x_1 : E), cexp (↑x * ↑⟪x_1, a⟫ * I) ∂μ = ∫ (x_1 : E), cexp (↑x * ↑⟪a, x_1⟫ * I) ∂μ
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
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
g g' : E →C_c ℝ
x✝ : FiniteMeasure E
⊢ ∫ (a : E), g a ∂↑x✝ + ∫ (a : E), g' a ∂↑x✝ = ∫ (x : E), g x ∂↑x✝ + ∫ (x : E), g' x ∂↑x✝

pp: case hf
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
g g' : E →C_c ℝ
x✝ : FiniteMeasure E
⊢ Integrable ⇑g ↑x✝

pp: case hg
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
g g' : E →C_c ℝ
x✝ : FiniteMeasure E
⊢ Integrable ⇑g' ↑x✝

Tactic:
]

Goal state after:
case hf
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
g g' : E →C_c ℝ
x✝ : FiniteMeasure E
⊢ Integrable ⇑g ↑x✝

case hg
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
g g' : E →C_c ℝ
x✝ : FiniteMeasure E
⊢ Integrable ⇑g' ↑x✝
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ i, |x i| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, |0 i| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ i, |(-x) i| ^ p) ^ (1 / p) = (∑ i, |x i| ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℝ), (∑ i, |(x + y) i| ^ p) ^ (1 / p) ≤ (∑ i, |x i| ^ p) ^ (1 / p) + (∑ i, |y i| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ i, |(r • x) i| ^ p) ^ (1 / p) ≤ |r| * (∑ i, |x i| ^ p) ^ (1 / p)
x✝ : ι → ℝ
⊢ ∑ i, |x✝ i| ^ p < 1 ↔ ∑ i, |x✝ i| ^ p < 1

pp: ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ i, |x i| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, |0 i| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ i, |(-x) i| ^ p) ^ (1 / p) = (∑ i, |x i| ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℝ), (∑ i, |(x + y) i| ^ p) ^ (1 / p) ≤ (∑ i, |x i| ^ p) ^ (1 / p) + (∑ i, |y i| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ i, |(r • x) i| ^ p) ^ (1 / p) ≤ |r| * (∑ i, |x i| ^ p) ^ (1 / p)
x✝ : ι → ℝ
⊢ 0 ≤ ∑ i, |x✝ i| ^ p

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ i, |x i| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, |0 i| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ i, |(-x) i| ^ p) ^ (1 / p) = (∑ i, |x i| ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℝ), (∑ i, |(x + y) i| ^ p) ^ (1 / p) ≤ (∑ i, |x i| ^ p) ^ (1 / p) + (∑ i, |y i| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ i, |(r • x) i| ^ p) ^ (1 / p) ≤ |r| * (∑ i, |x i| ^ p) ^ (1 / p)
x✝ : ι → ℝ
⊢ 0 ≤ ∑ i, |x✝ i| ^ p
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
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
c : ℝ
g : E →C_c ℝ
x✝ : FiniteMeasure E
⊢ c • ∫ (a : E), g a ∂↑x✝ = c • ∫ (x : E), g x ∂↑x✝

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3.e'_5
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ i, |x i| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, |0 i| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ i, |(-x) i| ^ p) ^ (1 / p) = (∑ i, |x i| ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℝ), (∑ i, |(x + y) i| ^ p) ^ (1 / p) ≤ (∑ i, |x i| ^ p) ^ (1 / p) + (∑ i, |y i| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ i, |(r • x) i| ^ p) ^ (1 / p) ≤ |r| * (∑ i, |x i| ^ p) ^ (1 / p)
⊢ (2 * Gamma (1 / p + 1)) ^ card ι = (2 * Gamma (1 / p + 1)) ^ card ι

Tactic:
]

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
⊢ (μlim univ).toNNReal ≤ (ENNReal.ofReal ↑C).toNNReal

Tactic:
]

Goal state after:
case refine_1
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
⊢ (μlim univ).toNNReal ≤ (ENNReal.ofReal ↑C).toNNReal
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3.e'_6
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ i, |x i| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, |0 i| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ i, |(-x) i| ^ p) ^ (1 / p) = (∑ i, |x i| ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℝ), (∑ i, |(x + y) i| ^ p) ^ (1 / p) ≤ (∑ i, |x i| ^ p) ^ (1 / p) + (∑ i, |y i| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ i, |(r • x) i| ^ p) ^ (1 / p) ≤ |r| * (∑ i, |x i| ^ p) ^ (1 / p)
⊢ ↑(card ι) / p + 1 = ↑(card ι) / p + 1

Tactic:
]

Goal state after:
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
inst✝ : CompactSpace E
C : ℝ≥0
this : {μ | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C}
⊢ IsCompact ({μ | μ.mass ≤ C} ∩ {μ | μ.mass = C})

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
this : {μ | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C}
⊢ IsCompact ({μ | μ.mass ≤ C} ∩ {μ | μ.mass = C})
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
this : {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ∅
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal (r ^ finrank ℝ (ι → ℝ)) * volume {x | ∑ i, |x i| ^ p < 1}

Tactic:
]

Goal state after:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal (r ^ finrank ℝ (ι → ℝ)) * volume {x | ∑ i, |x i| ^ p < 1}
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑(FiniteMeasure.comap f μ) (Subtype.val ⁻¹' s) = ↑μ s

Tactic:
]

Goal state after:
case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑(FiniteMeasure.comap f μ) (Subtype.val ⁻¹' s) = ↑μ s
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑μ (s ∩ range Subtype.val) = ↑μ s

pp: case h₁.hf
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val '' s)

pp: case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val ⁻¹' s)

Tactic:
]

Goal state after:
case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑μ (s ∩ range Subtype.val) = ↑μ s

case h₁.hf
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val '' s)

case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑μ s = ↑μ s

pp: case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂↑μ, x ∈ range Subtype.val

Tactic:
]

Goal state after:
case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂↑μ, x ∈ range Subtype.val
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ μ Kᶜ = 0

Tactic:
]

Goal state after:
case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ μ Kᶜ = 0
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₂
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure ↑K
hμ : μ.mass ≤ C
⊢ (μ.map f).mass ≤ C ∧ ↑μ (f ⁻¹' Kᶜ) = 0

Tactic:
]

Goal state after:
case h₂
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure ↑K
hμ : μ.mass ≤ C
⊢ (μ.map f).mass ≤ C ∧ ↑μ (f ⁻¹' Kᶜ) = 0
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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
this : {μ | μ.mass ≤ C ∧ μ Kᶜ = 0} = F '' T
⊢ IsCompact (F '' T)

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
this : {μ | μ.mass ≤ C ∧ μ Kᶜ = 0} = F '' T
⊢ IsCompact (F '' T)
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
μ : FiniteMeasure E
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)

pp: case hd
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
μ : FiniteMeasure E
n : ℕ
⊢ (↑(Finset.range (n + 1))).Pairwise (Function.onFun Disjoint (disjointed K))

pp: case hm
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
μ : FiniteMeasure E
n : ℕ
⊢ ∀ (i : ℕ), MeasurableSet (disjointed K i)

Tactic:
]

Goal state after:
case hd
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
μ : FiniteMeasure E
n : ℕ
⊢ (↑(Finset.range (n + 1))).Pairwise (Function.onFun Disjoint (disjointed K))

case hm
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
μ : FiniteMeasure E
n : ℕ
⊢ ∀ (i : ℕ), MeasurableSet (disjointed K i)