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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
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}
⊢ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0} = F '' T

Tactic:
apply Subset.antisymm

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 := ⋯
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := ⋯
T : Set (FiniteMeasure ↑K) := ⋯
⊢ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0} ⊆ F '' T

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 := ⋯
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := ⋯
T : Set (FiniteMeasure ↑K) := ⋯
⊢ F '' T ⊆ {μ | μ.mass ≤ C ∧ μ 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
n : ℕ
⊢ IsCompact ((partialSups K) n)

Tactic:
simpa using

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
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
n : ℕ
⊢ IsCompact (accumulate K n)
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: case neg
ι : 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
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((∏ c, (s c).indicator (fun x ↦ 1) (p.1 c)) * ∏ c, (t c).indicator (fun x ↦ 1) (p.2 c)))
x : (i : ι) → X i
hy : x ∉ univ.pi s
⊢ (∏ i, if x i ∈ s i then 1 else 0) = 0

Tactic:
simpa using

Goal state after:
case neg
ι : 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
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((∏ c, (s c).indicator (fun x ↦ 1) (p.1 c)) * ∏ c, (t c).indicator (fun x ↦ 1) (p.2 c)))
x : (i : ι) → X i
hy : x ∉ univ.pi s
⊢ ∃ a, x a ∉ s a
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝¹ : PseudoMetricSpace E
inst✝ : ProperSpace E
x : E
h✝ : ∀ ε > 0, ∃ N, ∀ n ≥ N, ⨆ μ ∈ S, μ (Metric.closedBall x n)ᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ
h : ∀ n ≥ r, ⨆ μ ∈ S, μ (Metric.closedBall x n)ᶜ ≤ ε
⊢ ∀ μ ∈ S, μ (Metric.closedBall x r)ᶜ ≤ ε

Tactic:
simpa using

Goal state after:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝¹ : PseudoMetricSpace E
inst✝ : ProperSpace E
x : E
h✝ : ∀ ε > 0, ∃ N, ∀ n ≥ N, ⨆ μ ∈ S, μ (Metric.closedBall x n)ᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ
h : ∀ n ≥ r, ⨆ μ ∈ S, μ (Metric.closedBall x n)ᶜ ≤ ε
⊢ ∀ μ ∈ S, μ (Metric.closedBall x r)ᶜ ≤ ε
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : ProperSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖x‖}) atTop) atTop (𝓝 0)
n : ℕ
h_tight : Tendsto (fun r ↦ ⨆ μ_1 ∈ {μ n}, μ_1 {x | r < ‖x‖}) atTop (𝓝 0)
⊢ Tendsto (fun r ↦ (μ n) {x | r < ‖x‖}) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : ProperSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖x‖}) atTop) atTop (𝓝 0)
n : ℕ
h_tight : Tendsto (fun r ↦ ⨆ μ_1 ∈ {μ n}, μ_1 {x | r < ‖x‖}) atTop (𝓝 0)
⊢ Tendsto (fun r ↦ (μ n) {x | r < ‖x‖}) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
a b : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst✝ : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ∫ᶜ (x : E) in Path.segment a b, ω x + ∫ᶜ (x : E) in Path.segment b x, ω x) (ω b) s b

Tactic:
refine .const_add _ <| ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
a b : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst✝ : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ∫ᶜ (x : E) in Path.segment b x, ω x) (ω b) s b
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
⊢ Nonempty ι

Tactic:
simpa using

Goal state after:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
⊢ Nonempty ι
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case hdω
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
ha : a ∈ s
x y : 𝕜
⊢ ((ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton 𝕜 (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1) (derivWithin f s a))))
        x)
      y =
    ((ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton 𝕜 (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1) (derivWithin f s a))))
        y)
      x

Tactic:
simpa using

Goal state after:
case hdω
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
ha : a ∈ s
x y : 𝕜
⊢ x • y • derivWithin f s a = y • x • derivWithin f s a
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
z : E
n : ℕ
h_tight : Tendsto (fun r ↦ ⨆ μ_1 ∈ {Measure.map (fun x ↦ ⟪z, x⟫_𝕜) (μ n)}, μ_1 {x | r < ‖x‖}) atTop (𝓝 0)
h_map : ∀ (r : ℝ), (Measure.map (fun x ↦ ⟪z, x⟫_𝕜) (μ n)) {x | r < ‖x‖} = (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}
⊢ Tendsto (fun r ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
z : E
n : ℕ
h_tight : Tendsto (fun r ↦ ⨆ μ_1 ∈ {Measure.map (fun x ↦ ⟪z, x⟫_𝕜) (μ n)}, μ_1 {x | r < ‖x‖}) atTop (𝓝 0)
h_map : ∀ (r : ℝ), (Measure.map (fun x ↦ ⟪z, x⟫_𝕜) (μ n)) {x | r < ‖x‖} = (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}
⊢ Tendsto (fun r ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n) Set.univ ≤ ↑C
z : E
hz : ‖z‖ = 1
h_ofReal :
  ∀ (r : ℝ),
    limsup (fun n ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop =
      ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫_𝕜‖}) atTop)
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n) Set.univ ≤ ↑C
z : E
hz : ‖z‖ = 1
h_ofReal :
  ∀ (r : ℝ),
    limsup (fun n ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop =
      ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫_𝕜‖}) atTop)
⊢ Tendsto (fun r ↦ ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫_𝕜‖}) atTop)) atTop (𝓝 (ENNReal.ofReal 0))
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 < ε✝
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : μ (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
Dne : D.Nonempty
f : ℕ → Set α
hD : μ (⋂ n, (accumulate f n)ᶜ) = 0
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ n, accumulate f n
i j : ℕ
hij : i ≤ j
⊢ (accumulate f j)ᶜ ⊆ (accumulate f i)ᶜ

Tactic:
simpa using

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 < ε✝
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : μ (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
Dne : D.Nonempty
f : ℕ → Set α
hD : μ (⋂ n, (accumulate f n)ᶜ) = 0
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ n, accumulate f n
i j : ℕ
hij : i ≤ j
⊢ accumulate f i ⊆ accumulate f j
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 : 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
x y : E
⊢ 1 y ≤ g x + 1

Tactic:
simpa using

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 : 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
x y : E
⊢ 0 ≤ g x
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 : 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
x y : E
⊢ 1 x ≤ 1 + g y

Tactic:
simpa using

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 : 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
x y : E
⊢ 0 ≤ g y
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)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
hf_tendsto : ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : E⦄, dist x 0 < δ → dist (f x) (f 0) < ε
ε : ℝ
hε : ε > 0
⊢ 1 = f 0

Tactic:
simpa using

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)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
hf_tendsto : ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : E⦄, dist x 0 < δ → dist (f x) (f 0) < ε
ε : ℝ
hε : ε > 0
⊢ 1 = f 0
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition ⟨s, hs⟩
⊢ ∑ p ∈ P.parts, f ↑p ≤ preVariationFun f s

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition ⟨s, hs⟩
⊢ ∀ (b : ℝ≥0∞), (∀ (i : Finpartition ⟨s, ⋯⟩), ∑ p ∈ i.parts, f ↑p ≤ b) → ∑ p ∈ P.parts, f ↑p ≤ b
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun p ↦ (fun i ↦ p.1 i, fun x ↦ p.2), invFun := fun p ↦ (fun i ↦ p.1 i, p.2 ()), left_inv := ⋯,
    right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
f : (i : ι) → X i →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : ((i : ι) → X i) × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (x : ((i : ι) → X i) × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂ν

Tactic:
simpa using

Goal state after:
ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun p ↦ (fun i ↦ p.1 i, fun x ↦ p.2), invFun := fun p ↦ (fun i ↦ p.1 i, p.2 ()), left_inv := ⋯,
    right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
f : (i : ι) → X i →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : ((i : ι) → X i) × T), (∏ x_1, (f x_1) (x.1 x_1)) * (g PUnit.unit) x.2 ∂μ =
    ∫ (x : ((i : ι) → X i) × T), (∏ x_1, (f x_1) (x.1 x_1)) * (g PUnit.unit) x.2 ∂ν