ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, εs i ≤ ε / 2 / 2 ^ Fintype.card ι<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<GOAL>∀ x ∈ {π | ∃ c, l.MemBaseSet I c (δ c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<GOAL>∀ (x : TaggedPrepartition I), (∃ c, l.MemBaseSet I c (δ c) x ∧ x.IsPartition) → integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<VAR>π : TaggedPrepartition I<VAR>c : ℝ≥0<VAR>hπδ : l.MemBaseSet I c (δ c) π<VAR>hπp : π.IsPartition<GOAL>integralSum f vol π ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<VAR>π : TaggedPrepartition I<VAR>c : ℝ≥0<VAR>hπδ : l.MemBaseSet I c (δ c) π<VAR>hπp : π.IsPartition<GOAL>dist (∑ x ∈ Finset.filter (fun J => π.tag J ∈ s) π.boxes, (vol x) (f (π.tag x)) + ∑ x ∈ Finset.filter (fun x => π.tag x ∉ s) π.boxes, (vol x) (f (π.tag x))) (∑ x ∈ Finset.filter (fun J => π.tag J ∈ s) π.boxes, g x + ∑ x ∈ Finset.filter (fun x => π.tag x ∉ s) π.boxes, g x) ≤ ε / 2 + ε / 2
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<VAR>π : TaggedPrepartition I<VAR>c : ℝ≥0<VAR>hπδ : l.MemBaseSet I c (δ c) π<VAR>hπp : π.IsPartition<GOAL>dist (∑ x ∈ Finset.filter (fun J => π.tag J ∈ s) π.boxes, (vol x) (f (π.tag x))) (∑ x ∈ Finset.filter (fun J => π.tag J ∈ s) π.boxes, g x) ≤ ε / 2
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε0' : 0 < ε / 2<VAR>H0 : 0 < 2 ^ Fintype.card ι<VAR>εs : (ι → ℝ) → ℝ<VAR>hεs0 : ∀ (i : ι → ℝ), 0 < εs i<VAR>hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2<VAR>ε' : ℝ<VAR>ε'0 : 0 < ε'<VAR>hεI : B I * ε' < ε / 2<VAR>δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'<VAR>π : TaggedPrepartition I<VAR>c : ℝ≥0<VAR>hπδ : l.MemBaseSet I c (δ c) π<VAR>hπp : π.IsPartition<GOAL>dist (∑ x ∈ Finset.filter (fun x => π.tag x ∉ s) π.boxes, (vol x) (f (π.tag x))) (∑ x ∈ Finset.filter (fun x => π.tag x ∉ s) π.boxes, g x) ≤ ε / 2
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>a : A<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : NoZeroDivisors R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>p : R[X]<VAR>h : (aeval a) p = 0<VAR>h' : p ≠ 0<GOAL>IsTorsion R[X] (AEval R M a)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>a : A<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : NoZeroDivisors R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>p : R[X]<VAR>h : (aeval a) p = 0<VAR>h' : p ≠ 0<VAR>hp : p ∈ nonZeroDivisors R[X]<GOAL>IsTorsion R[X] (AEval R M a)
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>i : Fin n<VAR>hl : i.castSucc < a<VAR>hu : b < i.succ<GOAL>b < a
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>i : Fin n<VAR>hl : ↑i < ↑a<VAR>hu : ↑b < ↑i + 1<GOAL>↑b < ↑a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U : OpenAddSubgroup R<GOAL>∃ V, ↑V * ↑V ⊆ ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U V : OpenAddSubgroup R<VAR>H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U<GOAL>∃ V, ↑V * ↑V ⊆ ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U V : OpenAddSubgroup R<VAR>H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U<GOAL>↑V * ↑V ⊆ ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U V : OpenAddSubgroup R<VAR>H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U<VAR>v a : R<VAR>ha : a ∈ ↑V<VAR>b : R<VAR>hb : b ∈ ↑V<VAR>hv : (fun x x_1 => x * x_1) a b = v<GOAL>v ∈ ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U V : OpenAddSubgroup R<VAR>H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U<VAR>v a : R<VAR>ha : a ∈ ↑V<VAR>b : R<VAR>hb : b ∈ ↑V<VAR>hv : (fun x x_1 => x * x_1) a b = v<VAR>hy : (a, b) ∈ (fun p => p.1 * p.2) ⁻¹' ↑U<GOAL>v ∈ ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U V : OpenAddSubgroup R<VAR>H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U<VAR>v a : R<VAR>ha : a ∈ ↑V<VAR>b : R<VAR>hb : b ∈ ↑V<VAR>hv : (fun x x_1 => x * x_1) a b = v<VAR>hy : v ∈ U<GOAL>v ∈ ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : NonarchimedeanRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : TopologicalSpace S<VAR>inst✝ : NonarchimedeanRing S<VAR>U V : OpenAddSubgroup R<VAR>H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U<VAR>v a : R<VAR>ha : a ∈ ↑V<VAR>b : R<VAR>hb : b ∈ ↑V<VAR>hv : (fun x x_1 => x * x_1) a b = v<VAR>hy : v ∈ U<GOAL>v ∈ U
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>𝟙 c.pt ≫ c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<VAR>this : ((Functor.const (J × K)).obj c.pt).map (𝟙 j, f) ≫ c.π.app (j, k') = c.π.app (j, k) ≫ (uncurry.obj F).map (𝟙 j, f)<GOAL>c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<VAR>this : 𝟙 c.pt ≫ c.π.app (j, k') = c.π.app (j, k) ≫ (F.map (𝟙 j)).app k ≫ (F.obj j).map f<GOAL>c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<VAR>this : c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f<GOAL>c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<GOAL>(𝟙 c.pt ≫ (Q j').lift { pt := c.pt, π := { app := fun k => c.π.app (j', k), naturality := ⋯ } }) ≫ (D.obj j').π.app k = ((Q j).lift { pt := c.pt, π := { app := fun k => c.π.app (j, k), naturality := ⋯ } } ≫ (D.map f).hom) ≫ (D.obj j').π.app k
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<GOAL>c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k