ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : ∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true<VAR>b : α<VAR>hb : b ∈ l<GOAL>b = a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : ∀ (b : α), b ∈ l → a = b<VAR>b : α<VAR>hb : b ∈ l<GOAL>(b == a) = true
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : FiniteDimensional k V<VAR>n : ℕ<VAR>T : Simplex k V n<VAR>hrank : finrank k V = n<GOAL>affineSpan k (Set.range T.points) = ⊤
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<GOAL>1 < a ^ 2 ↔ 1 < |a|
<VAR>b✝ : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>Integrable (fun v => cexp (-∑ i : ι, b i * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) volume
<VAR>b✝ : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>Integrable (fun v => ∏ x : ι, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x))) volume
<VAR>b✝ : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<VAR>i : ι<GOAL>Integrable ((fun i v => cexp (-b i * ↑v ^ 2 + c i * ↑v)) i) volume
<VAR>b✝ : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<VAR>i : ι<VAR>x : ℝ<GOAL>-b i * ↑x ^ 2 + c i * ↑x = -b i * ↑x ^ 2 + c i * ↑x + 0
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff'✝ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg'✝ : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)<VAR>h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x<GOAL>∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff'✝ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg'✝ : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)<VAR>h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x<VAR>hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))<GOAL>∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff'✝ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg'✝ : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)<VAR>h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x<VAR>hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))<VAR>hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))<GOAL>∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff'✝ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg'✝ : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)<VAR>h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x<VAR>hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))<VAR>hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))<VAR>h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x<GOAL>∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff'✝ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg'✝ : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)<VAR>h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x<VAR>hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))<VAR>hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))<VAR>h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x<VAR>hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x<GOAL>∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff'✝ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg'✝ : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)<VAR>h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x<VAR>hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))<VAR>hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))<VAR>h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x<VAR>hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x<VAR>c : ℝ<VAR>cmem : c ∈ Ioo a b<VAR>hc : h' c = 0<GOAL>∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n✝ : ℕ<VAR>a : M<VAR>m n : ℕ<GOAL>(a ^ m) ^ n = (a ^ n) ^ m
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>S : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>r : R<GOAL>(algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>interior (sphere x r) = ∅
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<GOAL>polynomialFunctions s = Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<GOAL>polynomialFunctions s ≤ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<VAR>p : R[X]<GOAL>↑(toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<VAR>p : R[X]<GOAL>(toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<VAR>p : R[X]<VAR>r : R<GOAL>(toContinuousMapOnAlgHom s) (Polynomial.C r) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<VAR>p f g : R[X]<VAR>hf : (toContinuousMapOnAlgHom s) f ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}<VAR>hg : (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}<GOAL>(toContinuousMapOnAlgHom s) (f + g) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set R<VAR>p : R[X]<VAR>n : ℕ<VAR>r : R<VAR>hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}<GOAL>(toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}