ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>(((↑{ toLinearEquiv := (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x)) 1) (Fin.tail fun x => 1) = (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>i.castLT ⋯ ≤ j
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<VAR>h : r ≠ 0<GOAL>closure (ball x r) = closedBall x r
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : FG L M<VAR>f : M →[L] N<VAR>hs : Function.Surjective ⇑f<GOAL>FG L N
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : FG L M<VAR>f : M →[L] N<VAR>hs : f.range = ⊤<GOAL>FG L N
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : FG L M<VAR>f : M →[L] N<VAR>hs : f.range = ⊤<GOAL>f.range.FG
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<GOAL>(s1 ⊓ s2).direction ≤ s1.direction ⊓ s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<GOAL>Submodule.span k (↑(s1 ⊓ s2) -ᵥ ↑(s1 ⊓ s2)) ≤ Submodule.span k (↑s1 -ᵥ ↑s1) ⊓ Submodule.span k (↑s2 -ᵥ ↑s2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : ι → TopologicalSpace α<VAR>t₂ : TopologicalSpace β<GOAL>Continuous f ↔ ∀ (i : ι), Continuous f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝ : PseudoMetricSpace α✝<VAR>f✝ : ℕ → α✝<VAR>a : α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : β → ℝ<VAR>hf : 0 ≤ f<VAR>s : α → Set β<VAR>hs : ∀ (i : β), ∃! j, i ∈ s j<GOAL>Summable f ↔ (∀ (j : α), Summable fun i => f ↑i) ∧ Summable fun j => ∑' (i : ↑(s j)), f ↑i
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s t : 𝕜 → 𝕜<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>ht : MeromorphicOn t U<VAR>hf : MeromorphicOn f U<VAR>hg : MeromorphicOn g U<VAR>h : MeromorphicOn s⁻¹ U<GOAL>MeromorphicOn s U
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁵ : Category.{u_6, u_1} C₁<VAR>inst✝⁴ : Category.{u_5, u_2} C₂<VAR>inst✝³ : Category.{?u.45088, u_3} D₁<VAR>inst✝² : Category.{?u.45092, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G<VAR>hG : W.IsInvertedBy G<GOAL>G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁵ : Category.{u_6, u_1} C₁<VAR>inst✝⁴ : Category.{u_5, u_2} C₂<VAR>inst✝³ : Category.{?u.45088, u_3} D₁<VAR>inst✝² : Category.{?u.45092, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G<VAR>hG : W.IsInvertedBy G<VAR>this : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)<GOAL>G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁵ : Category.{u_6, u_1} C₁<VAR>inst✝⁴ : Category.{u_5, u_2} C₂<VAR>inst✝³ : Category.{?u.45088, u_3} D₁<VAR>inst✝² : Category.{?u.45092, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G<VAR>hG : W.IsInvertedBy G<VAR>this✝ : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)<VAR>this : IsIso (whiskerRight adj.unit W.Q)<GOAL>G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁵ : Category.{u_6, u_1} C₁<VAR>inst✝⁴ : Category.{u_5, u_2} C₂<VAR>inst✝³ : Category.{?u.45088, u_3} D₁<VAR>inst✝² : Category.{?u.45092, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G<VAR>hG : W.IsInvertedBy G<VAR>this✝ : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)<VAR>this : IsIso (whiskerRight adj.unit W.Q)<VAR>e : W.Localization ≌ C₂ := Equivalence.mk (lift G hG W.Q) (F ⋙ W.Q) (liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) (𝟭 W.Localization) (lift G hG W.Q ⋙ F ⋙ W.Q) (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q))) (F.associator W.Q (lift G hG W.Q) ≪≫ isoWhiskerLeft F (fac G hG W.Q) ≪≫ asIso adj.counit)<GOAL>G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ : α → Type u_4<VAR>a✝ : α<VAR>s✝ : Multiset α<VAR>t✝ : (a : α) → Multiset (σ a)<VAR>a : α<VAR>s : Multiset α<VAR>IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u<VAR>t u : (a : α) → Multiset (σ a)<GOAL>((a ::ₘ s).sigma fun a => t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ : α → Type u_4<VAR>a✝ : α<VAR>s✝ : Multiset α<VAR>t✝ : (a : α) → Multiset (σ a)<VAR>a : α<VAR>s : Multiset α<VAR>IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u<VAR>t u : (a : α) → Multiset (σ a)<GOAL>map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>e : Perm α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∈ Set.range ⇑f<GOAL>(e.extendDomain f.toEquivRange) b = f (e (⋯.invOfMemRange ⟨b, h⟩))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>e : Perm α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∈ Set.range ⇑f<GOAL>↑(f.toEquivRange (e (f.toEquivRange.symm ⟨b, ?h⟩))) = f (e (⋯.invOfMemRange ⟨b, h⟩))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>e : Perm α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∈ Set.range ⇑f<GOAL>b ∈ Set.range ⇑f
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>(l.set n a)[n]? = some a
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>(fun x => a) <$> some l[n] = some a
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>φ : L.Formula α<GOAL>M ⊨ equivSentence φ ↔ φ.Realize fun a => ↑(L.con a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>a : ℝ<GOAL>LocallyLipschitz fun x => max a (f x)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hf : IntegrableOn f (↑I) μ<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hf : IntegrableOn f (↑I) μ<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hf : IntegrableOn f (↑I) μ<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hf : IntegrableOn f (↑I) μ<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hf : IntegrableOn f (↑I) μ<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hf : IntegrableOn f (↑I) μ<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε