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 : ∀ (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<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) 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<VAR>Hid : IntegrableOn (fun x => f (i.insertNth d x) i) (Box.Icc (I.face i)) volume<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᶠ (x : ℕ) in atTop, dist (∫ (x : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth d x) i) (∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth (c x) x_1) i) ∈ Metric.closedBall 0 ε
<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<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j : Fin n, (J.upper j - J.lower j)<GOAL>∀ᶠ (x : ℕ) in atTop, dist (∫ (x : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth d x) i) (∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth (c x) x_1) i) ∈ Metric.closedBall 0 ε
<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<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j : Fin n, (J.upper j - J.lower j)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>hδ : ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)<GOAL>∀ᶠ (x : ℕ) in atTop, dist (∫ (x : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth d x) i) (∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth (c x) x_1) i) ∈ Metric.closedBall 0 ε
<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<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j : Fin n, (J.upper j - J.lower j)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>hδ : ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)<VAR>k : ℕ<VAR>hk : dist (c k) d < δ<GOAL>dist (∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) (∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) ∈ Metric.closedBall 0 ε
<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<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j : Fin n, (J.upper j - J.lower j)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>hδ : ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)<VAR>k : ℕ<VAR>hk : dist (c k) d < δ<VAR>Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i)<GOAL>dist (∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) (∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) ∈ Metric.closedBall 0 ε
<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<VAR>H : Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j : Fin n, (J.upper j - J.lower j)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>hδ : ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)<VAR>k : ℕ<VAR>hk : dist (c k) d < δ<VAR>Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i)<GOAL>‖∫ (a : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d a) i - f (i.insertNth (c k) a) i ∂volume‖ ≤ ε
<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✝ s t : Set α<GOAL>sᶜ =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] t
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>(p * q).smeval x = p.smeval x * q.smeval x
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>u ∈ p.toSubgraph.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>inst✝ : Fintype α<VAR>C : G.Coloring α<GOAL>s.card ≤ card α
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>s : Finset V<VAR>h : induce (↑s) G = ⊤<VAR>inst✝ : Fintype α<VAR>C : G.Coloring α<GOAL>s.card ≤ card α
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>s : Finset V<VAR>h : induce (↑s) G = ⊤<VAR>inst✝ : Fintype α<VAR>C : G.Coloring α<VAR>f : ⊤ ↪g G<GOAL>s.card ≤ card α
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>s : Finset V<VAR>h : induce (↑s) G = ⊤<VAR>inst✝ : Fintype α<VAR>C : G.Coloring α<VAR>f : ⊤ ↪g G<GOAL>s.card = card ↑↑s
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.201719}<VAR>α : Type u<VAR>ι : Type v<VAR>f : ι → Set α<GOAL>lift.{v, u} #↑(⋃ i, f i) ≤ lift.{u, v} #ι * ⨆ i, lift.{v, u} #↑(f i)
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.201719}<VAR>α : Type u<VAR>ι : Type v<VAR>f : ι → Set α<GOAL>(sum fun i => #↑(f i)) = sum fun i => lift.{v, u} #↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>H : a ∈ s<GOAL>insert a ∅ ∩ s = insert a ∅
<VAR>m n : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ m * n<GOAL>p ∣ m.natAbs ∨ p ∣ n.natAbs
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>f : X → Y<VAR>h : Continuous f<VAR>t : ↑I<GOAL>((γ.trans γ').map h) t = ((γ.map h).trans (γ'.map h)) t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>f : X → Y<VAR>h : Continuous f<VAR>t : ↑I<GOAL>f (if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩) = if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>x a : α<VAR>l : List α<VAR>h : x ∈ (a :: l).head?<GOAL>a :: l = x :: (a :: l).tail
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>x a : α<VAR>l : List α<VAR>h : a = x<GOAL>a :: l = x :: (a :: l).tail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>(∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : CommMonoid M<VAR>a b : M<VAR>h : a * b = 1<GOAL>IsUnit b
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : CommMonoid M<VAR>a b : M<VAR>h : b * a = 1<GOAL>IsUnit b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>n : ℕ<VAR>x✝ : 𝒜.Nonempty<VAR>t : Finset α<VAR>ht : t ⊆ ∅<VAR>s : Finset α<VAR>hs : s ∈ 𝒜<GOAL>∅ ∩ s = t
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<GOAL>(dualAnnihilator W).dualCoannihilator = W
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>v : V<GOAL>v ∉ W → v ∉ (dualAnnihilator W).dualCoannihilator
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>v : V<GOAL>v ∉ W → ¬∀ (φ : Module.Dual K V), (∀ w ∈ W, φ w = 0) → φ v = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>v : V<GOAL>(¬∀ (φ : Module.Dual K (V ⧸ W)), φ (Submodule.Quotient.mk v) = 0) → ¬∀ (φ : Module.Dual K V), (∀ w ∈ W, φ w = 0) → φ v = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>v : V<VAR>x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0<VAR>φ : Module.Dual K (V ⧸ W)<VAR>hφ : φ (Submodule.Quotient.mk v) ≠ 0<VAR>w : V<VAR>hw : w ∈ W<GOAL>(φ ∘ₗ mkQ W) w = 0
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>h : K ≤ K'<VAR>x y : ↥K<GOAL>(inclusion h) x = (inclusion h) y → x = y
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₂₃<VAR>inst✝ : RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>x : E<VAR>y : F<GOAL>‖(f x) y‖ ≤ ‖f.flip‖ * ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₂₃<VAR>inst✝ : RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>x : E<VAR>y : F<GOAL>‖(f x) y‖ ≤ ‖f.flip‖ * ‖y‖ * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : Filter α<VAR>s : Set α<GOAL>(∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₁ : Function.LeftInverse φ' φ<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>(f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M