mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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.Prokhorov

Goal state before:
pp: case refine_2.inl
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this✝ : (↑μ).InnerRegular
g : E → ℝ
g_cont : Continuous[inst✝², _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this : Tendsto (fun ρ ↦ ∫ (x : E), g x ∂↑ρ) (↑f) (𝓝 (∫ (x : E), g x ∂↑μ))
⊢ ∫ (x : E), g x ∂↑μ ≤ ↑(u n)

Tactic:
apply le_of_tendsto this

Goal state after:
case refine_2.inl
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⋯
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this✝ : (↑μ).InnerRegular
g : E → ℝ
g_cont : Continuous[inst✝², _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this : Tendsto (fun ρ ↦ ∫ (x : E), g x ∂↑ρ) (↑f) (𝓝 (∫ (x : E), g x ∂↑μ))
⊢ ∀ᶠ (c : FiniteMeasure E) in ↑f, ∫ (x : E), g x ∂↑c ≤ ↑(u n)
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

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

Tactic:
let e : (Z × (Π i, Y i)) ≃ᵐ ((Π i, Y i) × Z) := .prodComm
  rw [← e.map_measurableEquiv_injective.eq_iff]
  refine ext_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map_equiv, integral_map_equiv]
  simpa [e, mul_comm] using! h g f

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

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

Tactic:
apply le_of_tendsto this

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ IsClosed[inst✝¹] μ.support

Tactic:
[

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ IsClosed[inst✝¹] μ.support
Module: Mathlib.MeasureTheory.Measure.Prokhorov

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

Tactic:
this

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : MeasurableSpace 𝕜
a : A
inst✝⁵ : OpensMeasurableSpace 𝕜
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : CompleteSpace A
inst✝¹ : MeasurableSpace A
inst✝ : BorelSpace A
⊢ Measurable (resolvent a)

Tactic:
have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
  have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_domRestrict]
    convert continuous_const (y := (0 : A)) with x
    simp
  have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
  simpa using h1.measurable_piecewise h2 h3

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

Goal state before:
pp: case inl
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)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
⊢ indicatorConstLp p ⋯ hμt 0 = indicatorConstLp p ms hμs 0

Tactic:
[

Goal state after:
case inl
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)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
⊢ indicatorConstLp p ⋯ hμt 0 = indicatorConstLp p ms hμs 0
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormedDivisionRing A
inst✝ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this✝ : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
this : infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖
⊢ infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖

Tactic:
this

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormedDivisionRing A
inst✝ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this✝ : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
this : infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖
⊢ ‖(algebraMap 𝕜 A) x - a‖ ≤ ‖(algebraMap 𝕜 A) x - a‖
Module: Mathlib.MeasureTheory.Measure.Prokhorov

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

Tactic:
apply le_of_tendsto this

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
s✝ : Set E
a✝ : MeasurableSet s✝
⊢ ↑μ₀ s✝ = ↑μ' s✝

Tactic:
this

Goal state after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
s✝ : Set E
a✝ : MeasurableSet s✝
⊢ ↑μ₀ s✝ = ↑μ₀ s✝
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ✝ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ✝ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw : ⇑g = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a))
μ : Measure E
hμ : IsProbabilityMeasure μ
⊢ ∫ (x : E), g x ∂μ = w.coeff.sum fun a z ↦ z * ∫ (x : E), ↑(probChar (((innerₗ E) x) a)) ∂μ

Tactic:
[

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ✝ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ✝ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw : ⇑g = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a))
μ : Measure E
hμ : IsProbabilityMeasure μ
⊢ ∫ (x : E), g x ∂μ = w.coeff.sum fun a z ↦ z * ∫ (x : E), ↑(probChar (((innerₗ E) x) a)) ∂μ
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw : ⇑g = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a))
h_eq :
  ∀ (μ : Measure E),
    IsProbabilityMeasure μ → ∫ (x : E), g x ∂μ = w.coeff.sum fun a z ↦ z * ∫ (x : E), ↑(probChar (((innerₗ E) x) a)) ∂μ
⊢ Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))

Tactic:
[

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw : ⇑g = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a))
h_eq :
  ∀ (μ : Measure E),
    IsProbabilityMeasure μ → ∫ (x : E), g x ∂μ = w.coeff.sum fun a z ↦ z * ∫ (x : E), ↑(probChar (((innerₗ E) x) a)) ∂μ
⊢ Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (f : E →ᵇ ℂ), Tendsto (fun i ↦ ∫ (ω : E), f ω ∂↑(μ i)) atTop (𝓝 (∫ (ω : E), f ω ∂↑μ₀))
t : E
⊢ Tendsto (fun n ↦ charFun (↑(μ n)) t) atTop (𝓝 (charFun (↑μ₀) t))

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (f : E →ᵇ ℂ), Tendsto (fun i ↦ ∫ (ω : E), f ω ∂↑(μ i)) atTop (𝓝 (∫ (ω : E), f ω ∂↑μ₀))
t : E
⊢ Tendsto (fun n ↦ charFun (↑(μ n)) t) atTop (𝓝 (charFun (↑μ₀) t))
Module: Mathlib.MeasureTheory.Measure.SubFinite

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

Tactic:
[

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

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

Tactic:
this

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ.toFinite = 0 ↔ μ = 0

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ.toFinite = 0 ↔ μ = 0
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

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

Tactic:
[

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