ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedSemiring α<VAR>inst✝⁴ : LinearOrderedSemiring β<VAR>inst✝³ : FloorSemiring α<VAR>inst✝² : FloorSemiring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b<VAR>h₀ : 0 ≤ a ↔ 0 ≤ b<VAR>ha : a < 0<GOAL>⌊a⌋₊ = ⌊b⌋₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedSemiring α<VAR>inst✝⁴ : LinearOrderedSemiring β<VAR>inst✝³ : FloorSemiring α<VAR>inst✝² : FloorSemiring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b<VAR>h₀ : 0 ≤ a ↔ 0 ≤ b<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ = ⌊b⌋₊
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : StrictConvexSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < (μ univ).toReal * C
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : StrictConvexSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>h₀ : μ = 0<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < (μ univ).toReal * C
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : StrictConvexSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>h₀ : μ ≠ 0<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < (μ univ).toReal * C
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : StrictConvexSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>h₀ : μ ≠ 0<VAR>hμ : 0 < (μ univ).toReal<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < (μ univ).toReal * C
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : StrictConvexSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>h₀ : μ ≠ 0<VAR>hμ : 0 < (μ univ).toReal<VAR>H : ‖⨍ (x : α), f x ∂μ‖ < C<GOAL>‖∫ (x : α), f x ∂μ‖ < (μ univ).toReal * C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i<VAR>hi₁ : MeasurableSet i<VAR>hj₁ : MeasurableSet j<GOAL>(s.toMeasureOfLEZero i hi₁ hi) j = ↑⟨-↑s (i ∩ j), ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i<VAR>hi₁ : MeasurableSet i<VAR>hj₁ : MeasurableSet j<GOAL>↑⟨↑(-s) (i ∩ j), ⋯⟩ = ↑⟨-↑s (i ∩ j), ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i<VAR>hi₁ : MeasurableSet i<VAR>hj₁ : MeasurableSet j<GOAL>MeasurableSet j
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ : ℝ<VAR>hr₁ : r₁ ≠ 0<VAR>r₂ : ℝ<GOAL>Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ : ℝ<VAR>hr₁ : r₁ ≠ 0<VAR>r₂ : ℝ<GOAL>∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b < r₂ → ‖a‖ * p b < r₁ * r₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ : ℝ<VAR>hr₁ : r₁ ≠ 0<VAR>r₂ : ℝ<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ r₁<VAR>b : E<VAR>hb : p b < r₂<GOAL>0 < r₁
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<GOAL>dickson 1 1 p = X ^ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>h : 1 = (ZMod.castHom ⋯ R) 1<GOAL>dickson 1 1 p = X ^ p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>x : M<VAR>i : ι<VAR>hx : x ∈ ℳ i<GOAL>↑(((decompose ℳ) x) i) = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>h : AEMeasurable f μ<VAR>s : Set β<VAR>hfs : ∀ (x : α), f x ∈ s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>AEMeasurable (codRestrict f s hfs) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>h : AEMeasurable f μ<VAR>s : Set β<VAR>hfs : ∀ (x : α), f x ∈ s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>g : α → β<VAR>g_meas : Measurable g<VAR>hg : range g ⊆ s<VAR>fg : f =ᶠ[ae μ] g<GOAL>AEMeasurable (codRestrict f s hfs) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>h : AEMeasurable f μ<VAR>s : Set β<VAR>hfs : ∀ (x : α), f x ∈ s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>g : α → β<VAR>g_meas : Measurable g<VAR>hg : range g ⊆ s<VAR>fg : f =ᶠ[ae μ] g<GOAL>codRestrict f s hfs =ᶠ[ae μ] codRestrict g s ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>h : AEMeasurable f μ<VAR>s : Set β<VAR>hfs : ∀ (x : α), f x ∈ s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>g : α → β<VAR>g_meas : Measurable g<VAR>hg : range g ⊆ s<VAR>fg : f =ᶠ[ae μ] g<VAR>x : α<VAR>hx : f x = g x<GOAL>codRestrict f s hfs x = codRestrict g s ⋯ x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_bot : limsup u f = ⊥<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_bot : limsup v f = ⊥<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_top : limsup v f = ⊤<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<GOAL>limsup (u + v) f ≤ limsup u f + limsup v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<GOAL>∀ (z : ℝ), limsup u f + limsup v f < ↑z → limsup (u + v) f ≤ ↑z
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<VAR>x : ℝ<VAR>hx : limsup u f + limsup v f < ↑x<GOAL>limsup (u + v) f ≤ ↑x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<VAR>x : ℝ<VAR>hx : limsup u f + limsup v f < ↑x<VAR>y : ℝ<VAR>sum_lt_y : limsup u f + limsup v f < ↑y<VAR>y_lt_x : ↑y < ↑x<GOAL>limsup (u + v) f ≤ ↑x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<VAR>x : ℝ<VAR>hx : limsup u f + limsup v f < ↑x<VAR>y : ℝ<VAR>sum_lt_y : limsup u f + limsup v f < ↑y<VAR>y_lt_x : ↑y < ↑x<VAR>key₁ : limsup u f < ↑y - limsup v f<GOAL>limsup (u + v) f ≤ ↑x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<VAR>x : ℝ<VAR>hx : limsup u f + limsup v f < ↑x<VAR>y : ℝ<VAR>sum_lt_y : limsup u f + limsup v f < ↑y<VAR>y_lt_x : ↑y < ↑x<VAR>key₁ : limsup u f < ↑y - limsup v f<VAR>key₂ : limsup v f < limsup v f + ↑x - ↑y<GOAL>limsup (u + v) f ≤ ↑x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤<VAR>h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥<VAR>u_nbot : ⊥ < limsup u f<VAR>v_nbot : ⊥ < limsup v f<VAR>v_ntop : limsup v f < ⊤<VAR>limsup_v_real : ↑(limsup v f).toReal = limsup v f<VAR>x : ℝ<VAR>hx : limsup u f + limsup v f < ↑x<VAR>y : ℝ<VAR>sum_lt_y : limsup u f + limsup v f < ↑y<VAR>y_lt_x : ↑y < ↑x<VAR>key₁ : limsup u f < ↑y - limsup v f<VAR>key₂ : limsup v f < limsup v f + ↑x - ↑y<GOAL>↑y - limsup v f + (limsup v f + ↑x - ↑y) = ↑x
<VAR>α : Type u_1<VAR>l₁ l₂ : Lists' α true<VAR>H : ∀ a ∈ l₁.toList, a ∈ l₂<GOAL>l₁ ⊆ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : Lists' α true<VAR>H : ∀ a ∈ l₁.toList, a ∈ l₂<GOAL>ofList l₁.toList ⊆ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>G : ι → α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : ∀ (n : ι), EqOn (F n) (G n) s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : α<VAR>hx : x ∈ s<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, G n y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>G : ι → α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : ∀ (n : ι), EqOn (F n) (G n) s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : α<VAR>hx : x ∈ s<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∀ᶠ (n : ι) in p, ∀ y ∈ s ∩ t, (f y, G n y) ∈ u
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X✝ Y✝ : C<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) _auto✝<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>G.map f ≫ (fun X => (app X).inv) Y = (fun X => (app X).inv) X ≫ F.map f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X✝ Y✝ : C<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) _auto✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : (fun f => (app X).inv ≫ f ≫ (app Y).inv) ((app X).hom ≫ G.map f) = (fun f => (app X).inv ≫ f ≫ (app Y).inv) (F.map f ≫ (app Y).hom)<GOAL>G.map f ≫ (fun X => (app X).inv) Y = (fun X => (app X).inv) X ≫ F.map f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X✝ Y✝ : C<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) _auto✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f<GOAL>G.map f ≫ (fun X => (app X).inv) Y = (fun X => (app X).inv) X ≫ F.map f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Subsingleton β<VAR>f : α → β<GOAL>StronglyMeasurable f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Subsingleton β<VAR>f : α → β<VAR>f_sf : α →ₛ β := { toFun := f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }<GOAL>StronglyMeasurable f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Subsingleton β<VAR>f : α → β<VAR>x : β<GOAL>MeasurableSet (f ⁻¹' {x})
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(freeOn E).Indep I ↔ I ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b✝ : β<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>GameAdd rα s(b, a₁) s(a₂, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b✝ : β<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>GameAdd rα s(a₁, b) s(a₂, b)
<VAR>x y : ℝ≥0<GOAL>0 < sqrt x ↔ 0 < x
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(cexp (↑x * I)).re = Real.cos x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝ : IsEmpty β<GOAL>Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝ : Nonempty β<GOAL>Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>h✝ : Nonempty β<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) ⊥ (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>Tendsto (fun x => ∑' (k : β), f x k) ⊥ (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<GOAL>Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<GOAL>Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<GOAL>Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<GOAL>∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<GOAL>∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<GOAL>∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<GOAL>∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε