ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>mα : MeasurableSpace α<VAR>f : α → E<VAR>hf : StronglyMeasurable f<VAR>a : α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : Decidable (a ∈ s)<GOAL>(∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<GOAL>countP p l₁ = countP p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<GOAL>(List.filter p l₁).length = (List.filter p l₂).length
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g f : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure 0<GOAL>∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂0 ∂0 = ∫⁻ (x : α), f x ∂0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<GOAL>∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : CommMonoid N<VAR>inst✝³ : DivisionCommMonoid G<VAR>k✝ l : ℕ+<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>p k : ℕ<VAR>m : ℕ+<VAR>inst✝ : ExpChar R p<VAR>ζ : Rˣ<GOAL>ζ ^ (p ^ k * ↑m) = 1 ↔ ζ ∈ rootsOfUnity m R
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X : C<VAR>S : Sieve X<GOAL>S ∈ (topologyOfClosureOperator J₁.closureOperator ⋯).sieves X ↔ S ∈ J₁.sieves X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s✝ t : Set α<VAR>h : Semiconj f fa fb<VAR>s : Set β<VAR>hb : InjOn fb s<VAR>hf : InjOn f (f ⁻¹' s)<VAR>x : α<VAR>hx : x ∈ f ⁻¹' s<VAR>y : α<VAR>hy : y ∈ f ⁻¹' s<VAR>H : fa x = fa y<VAR>this : f (fa x) = f (fa y)<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s✝ t : Set α<VAR>h : Semiconj f fa fb<VAR>s : Set β<VAR>hb : InjOn fb s<VAR>hf : InjOn f (f ⁻¹' s)<VAR>x : α<VAR>hx : x ∈ f ⁻¹' s<VAR>y : α<VAR>hy : y ∈ f ⁻¹' s<VAR>H : fa x = fa y<VAR>this : fb (f x) = fb (f y)<GOAL>x = y
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>Φ : Quotient r ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂<GOAL>Φ = lift r (functor r ⋙ Φ) H
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>Φ : Quotient r ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂<GOAL>∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>Φ : Quotient r ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂<GOAL>∀ (X Y : Quotient r) (f : X ⟶ Y), HEq (Φ.map f) ((lift r (functor r ⋙ Φ) H).map f)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>d : n → R<GOAL>(diagonal d).det = ∏ i : n, d i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>d : n → R<GOAL>∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = ∏ i : n, d i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>d : n → R<GOAL>∀ b ∈ univ, b ≠ 1 → ↑↑(sign b) * ∏ i : n, diagonal d (b i) i = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>d : n → R<GOAL>1 ∉ univ → ↑↑(sign 1) * ∏ i : n, diagonal d (1 i) i = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>d : n → R<GOAL>↑↑(sign 1) * ∏ i : n, diagonal d (1 i) i = ∏ i : n, d i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>{x_1 | (ker f).Rel x_1 x} ∈ Set.range fun y => {x | f x = y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>∃ y, {x | f x = y} = {x_1 | (ker f).Rel x_1 x}
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<GOAL>limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<GOAL>∀ (ε : ℝ≥0), 0 < ε → μ F < ⊤ → limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_lim : Tendsto rs atTop (𝓝 0)<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>rs_lim : (fun r => μ (Metric.cthickening r F)) ⁻¹' Iio (μ F + ↑ε) ∈ map rs atTop<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>rs_lim : ∃ a, ∀ b ≥ a, μ (Metric.cthickening (rs b) F) < μ F + ↑ε<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, μ (Metric.cthickening (rs b) F) < μ F + ↑ε<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, μ (Metric.cthickening (rs b) F) < μ F + ↑ε<VAR>aux' : ∀ (i : ι), (μs i) F ≤ (μs i) (Metric.thickening (rs m) F)<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, μ (Metric.cthickening (rs b) F) < μ F + ↑ε<VAR>aux' : ∀ (i : ι), (μs i) F ≤ (μs i) (Metric.thickening (rs m) F)<VAR>aux : (fun i => (μs i) F) ≤ᶠ[L] fun i => (μs i) (Metric.thickening (rs m) F)<GOAL>limsup (fun i => (μs i) F) L ≤ μ F + ↑ε
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, μ (Metric.cthickening (rs b) F) < μ F + ↑ε<VAR>aux' : ∀ (i : ι), (μs i) F ≤ (μs i) (Metric.thickening (rs m) F)<VAR>aux : (fun i => (μs i) F) ≤ᶠ[L] fun i => (μs i) (Metric.thickening (rs m) F)<GOAL>limsup (fun i => (μs i) (Metric.thickening (rs m) F)) L ≤ μ F + ↑ε