ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<VAR>hI_tendsto : Tendsto (fun k => ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i) atTop (𝓝 (∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i))<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<VAR>hI_tendsto : Tendsto (fun k => ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i) atTop (𝓝 (∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i))<GOAL>Tendsto (fun x => ∑ i : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).upper i) x_1) i) - ∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).lower i) x_1) i)) atTop (𝓝 (∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)<VAR>hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<GOAL>Tendsto (fun x => ∑ i : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).upper i) x_1) i) - ∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).lower i) x_1) i)) atTop (𝓝 (∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))<VAR>hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<GOAL>Tendsto (fun x => ∑ i : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).upper i) x_1) i) - ∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).lower i) x_1) i)) atTop (𝓝 (∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))<VAR>hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<GOAL>∀ (i : Fin (n + 1)) (c : ℕ → ℝ) (d : ℝ), (∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)) → Tendsto c atTop (𝓝 d) → Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))<VAR>hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<VAR>i : Fin (n + 1)<VAR>c : ℕ → ℝ<VAR>d : ℝ<VAR>hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)<VAR>hcd : Tendsto c atTop (𝓝 d)<GOAL>Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))<VAR>hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<VAR>i : Fin (n + 1)<VAR>c : ℕ → ℝ<VAR>d : ℝ<VAR>hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)<VAR>hcd : Tendsto c atTop (𝓝 d)<VAR>hd : d ∈ Set.Icc (I.lower i) (I.upper i)<GOAL>Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))<VAR>hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<VAR>i : Fin (n + 1)<VAR>c : ℕ → ℝ<VAR>d : ℝ<VAR>hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)<VAR>hcd : Tendsto c atTop (𝓝 d)<VAR>hd : d ∈ Set.Icc (I.lower i) (I.upper i)<VAR>Hic : ∀ (k : ℕ), IntegrableOn (fun x => f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume<GOAL>Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>J : ℕ →o Box (Fin (n + 1))<VAR>hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I<VAR>hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))<VAR>hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))<VAR>hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I<VAR>hJ_le : ∀ (k : ℕ), J k ≤ I<VAR>HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))<VAR>HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x<VAR>HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume<VAR>HJ_eq : ∀ (k : ℕ), ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)<VAR>i : Fin (n + 1)<VAR>c : ℕ → ℝ<VAR>d : ℝ<VAR>hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)<VAR>hcd : Tendsto c atTop (𝓝 d)<VAR>hd : d ∈ Set.Icc (I.lower i) (I.upper i)<VAR>Hic : ∀ (k : ℕ), IntegrableOn (fun x => f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume<VAR>Hid : IntegrableOn (fun x => f (i.insertNth d x) i) (Box.Icc (I.face i)) volume<GOAL>Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))