mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Tendsto Ps atTop (𝓝 P)

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto]

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.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ ∫ (x : X), K.indicator 1 x ∂μ ≤ ∫ (x : X), f x ∂μ

Tactic:
refine integral_mono ?_ f.integrable hfK

Goal state after:
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ Integrable (K.indicator 1) μ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ ν.real V ≤ (ν K).toReal + ↑ε

Tactic:
measureReal_def,

Goal state after:
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ (ν V).toReal ≤ (ν K).toReal + ↑ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := (fun J ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ i ⊆ Iio N,
    ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)
⊢ levyProkhorovDist ↑(ofMeasure P).toMeasure ↑(ofMeasure Q).toMeasure ≤ 2 * (ε / 3)

Tactic:
apply levyProkhorovDist_le_of_forall_le _ _ (by linarith) (fun δ B δ_gt _ ↦ ?_)

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := (fun J ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ i ⊆ Iio N,
    ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
x✝ : MeasurableSet B
⊢ ↑(ofMeasure P).toMeasure B ≤ ↑(ofMeasure Q).toMeasure (thickening δ B) + ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inl
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Subsingleton E
⊢ μ {0} = ENNReal.ofReal (μ.real {0})

Tactic:
measureReal_def,

Goal state after:
case inl
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Subsingleton E
⊢ μ {0} = ENNReal.ofReal (μ {0}).toReal
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ = 2 * ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ

Tactic:
by
    rw [← integral_const_mul]
    congr with _
    rw [mul_inv_cancel₀ (by positivity)]

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

Goal state before:
pp: case e'_2
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
p✝ : ℝ
hp : 0 < p✝
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 := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x < 1} = ν (Metric.ball 0 1)

Tactic:
@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball

Goal state after:
case e'_2
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
p✝ : ℝ
hp : 0 < p✝
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 := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x < 1} = μ (⇑φ ⁻¹' Metric.ball 0 1)

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
p✝ : ℝ
hp : 0 < p✝
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 := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ Measurable ⇑φ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
⊢ μ = ν

Tactic:
have hμν : μ univ = ν univ := by convert! h 1 1 <;> simp

Goal state after:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
⊢ μ = ν
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
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 := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x < r} = ν (Metric.ball 0 r)

Tactic:
@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball

Goal state after:
case e'_3
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 := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x < r} = μ (⇑φ ⁻¹' Metric.ball 0 r)

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 := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ Measurable ⇑φ
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:
exact ENNReal.toNNReal_mono (by simp) μlim_le

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
⊢ -(2 * r⁻¹) ≤ 2 * r⁻¹

Tactic:
rw [neg_le_self_iff]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
⊢ 0 ≤ 2 * r⁻¹
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
r : ℝ
hr : 0 < r
⊢ -(2 * r⁻¹) ≤ 2 * r⁻¹

Tactic:
rw [neg_le_self_iff]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
r : ℝ
hr : 0 < r
⊢ 0 ≤ 2 * r⁻¹
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ Continuous fun s ↦ μ ↑s

Tactic:
by
  refine continuous_of_le_add_edist 1 ENNReal.one_ne_top fun s t ↦ ?_
  rw [one_mul, ← tsub_le_iff_left]
  exact sub_le_edist s t

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁹ : (i : ι) → TopologicalSpace (X i)
inst✝⁸ : ∀ (i : ι), BorelSpace (X i)
inst✝⁷ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁶ : (j : κ) → TopologicalSpace (Y j)
inst✝⁵ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁴ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝³ : Fintype ι
inst✝² : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂μ =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂ν
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
this :
  ∀ {μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))},
    (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂μ).toReal =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂μ
⊢ (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ i, ↑((g i) (p.2 i)) ∂μ).toReal =
    (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ i, ↑((g i) (p.2 i)) ∂ν).toReal

Tactic:
simp_rw [this]

Goal state after:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁹ : (i : ι) → TopologicalSpace (X i)
inst✝⁸ : ∀ (i : ι), BorelSpace (X i)
inst✝⁷ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁶ : (j : κ) → TopologicalSpace (Y j)
inst✝⁵ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁴ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝³ : Fintype ι
inst✝² : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂μ =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂ν
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
this :
  ∀ {μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))},
    (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂μ).toReal =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂μ
⊢ ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂μ =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂ν
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
A : ∀ (i : ℕ), ∃ t ∈ C, μ (t ∆ f i) < δ i
⊢ ∃ t ∈ C, μ (t ∆ ⋃ i, f i) < ε

Tactic:
choose! t tC ht using A

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : ℕ → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), μ (t i ∆ f i) < δ i
⊢ ∃ t ∈ C, μ (t ∆ ⋃ i, f i) < ε
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
h : MeasurableSet s
⊢ preVariationFun f s = ⨆ P, ∑ p ∈ P.parts, f ↑p

Tactic:
by
  simp [preVariationFun, h]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
h : ¬MeasurableSet s
⊢ preVariationFun f s = 0

Tactic:
by
  simp [preVariationFun, h]

Goal state after: