ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (F.rightDerivedToHomotopyCategory.map f) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (J.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) = ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
<VAR>u : XgcdType<VAR>hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y<GOAL>u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y
<VAR>u : XgcdType<VAR>hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y<GOAL>u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c T : ℝ<VAR>hT : 0 ≤ T<VAR>vert_norm_bound : ∀ {T : ℝ}, 0 ≤ T → ∀ {c y : ℝ}, |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))<GOAL>‖verticalIntegral b c T‖ ≤ 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c T : ℝ<VAR>hT : 0 ≤ T<VAR>vert_norm_bound : ∀ {T : ℝ}, 0 ≤ T → ∀ {c y : ℝ}, |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))<GOAL>?m.32390 * |c - 0| ≤ 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c T : ℝ<VAR>hT : 0 ≤ T<VAR>vert_norm_bound : ∀ {T : ℝ}, 0 ≤ T → ∀ {c y : ℝ}, |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))<GOAL>ℝ
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c T : ℝ<VAR>hT : 0 ≤ T<VAR>vert_norm_bound : ∀ {T : ℝ}, 0 ≤ T → ∀ {c y : ℝ}, |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))<GOAL>∀ x ∈ Ι 0 c, ‖I * (cexp (-b * (↑T + ↑x * I) ^ 2) - cexp (-b * (↑T - ↑x * I) ^ 2))‖ ≤ ?m.32390
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>hab : a ≠ b<GOAL>(f a)! * (f b)! * multinomial {a, b} f = (f a + f b)!
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<GOAL>StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<VAR>H : StableUnderSpecialization s<GOAL>∀ s_1 ∈ (fun x => closure {x}) '' s, IsClosed s_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<VAR>H : StableUnderSpecialization s<GOAL>⋃₀ ((fun x => closure {x}) '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : KleeneAlgebra α<VAR>a b c : α<VAR>h : a∗ = a<GOAL>a * a = a
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type u_11<VAR>N : Type u_12<VAR>inst✝⁴ : Monoid N<VAR>inst✝³ : SMul M N<VAR>inst✝² : MulAction N α<VAR>inst✝¹ : SMul M α<VAR>inst✝ : IsScalarTower M N α<VAR>x : M<VAR>y : α<GOAL>(x • 1) • y = x • y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<GOAL>∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<GOAL>S.SupIndep fun i => torsionBy R M (q i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<VAR>x✝ : ι<GOAL>torsionBy R M (q x✝) = torsionBySet R M ↑(Ideal.span {q x✝})
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>x : α<VAR>h : Bornology.IsBounded (range fun x_1 => g (f^[x_1] x))<GOAL>Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>x : α<VAR>h : Bornology.IsBounded (range fun x_1 => g (f^[x_1] x))<VAR>C : ℝ<VAR>hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C<GOAL>Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>x : α<VAR>h : Bornology.IsBounded (range fun x_1 => g (f^[x_1] x))<VAR>C : ℝ<VAR>hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C<VAR>this : Tendsto (fun n => C / ↑n) atTop (𝓝 0)<GOAL>Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>x : α<VAR>h : Bornology.IsBounded (range fun x_1 => g (f^[x_1] x))<VAR>C : ℝ<VAR>hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C<VAR>this : Tendsto (fun n => C / ↑n) atTop (𝓝 0)<VAR>n : ℕ<GOAL>‖birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x‖ ≤ C / ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>x : α<VAR>h : Bornology.IsBounded (range fun x_1 => g (f^[x_1] x))<VAR>C : ℝ<VAR>hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C<VAR>this : Tendsto (fun n => C / ↑n) atTop (𝓝 0)<VAR>n : ℕ<GOAL>dist (g (f^[n] x)) (g x) / ↑n ≤ C / ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>inst✝ : CompleteSpace F<GOAL>ContinuousOn p.sum (EMetric.ball 0 p.radius)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>inst✝ : CompleteSpace F<VAR>h : 0 = p.radius<GOAL>ContinuousOn p.sum (EMetric.ball 0 p.radius)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>inst✝ : CompleteSpace F<VAR>h : 0 < p.radius<GOAL>ContinuousOn p.sum (EMetric.ball 0 p.radius)
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U V : Y.Opens<VAR>e : U = V<GOAL>Hom.app f U = Y.presheaf.map (eqToHom ⋯).op ≫ Hom.app f V ≫ X.presheaf.map (eqToHom ⋯).op
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U V : Y.Opens<VAR>e : U = V<GOAL>f.val.c.app (op V) ≫ ((Presheaf.pushforward CommRingCat f.val.base).obj X.presheaf).map (inv (eqToHom ⋯).op) = Hom.app f V ≫ X.presheaf.map (eqToHom ⋯).op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : β → E<VAR>μ : Measure β<VAR>a : α<GOAL>∫ (x : β), f x ∂(const α μ) a = ∫ (x : β), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>x : A<GOAL>‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x‖ = ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Ioi a)<GOAL>Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Ioi a)<GOAL>Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
<VAR>S : Set ℝ<VAR>h₁ : S.Nonempty<VAR>h₂ : BddAbove S<GOAL>IsLUB S (sSup S)
<VAR>S : Set ℝ<VAR>h₁ : S.Nonempty<VAR>h₂ : BddAbove S<GOAL>IsLUB S (Classical.choose ⋯)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a : ℕ → ℝ<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) → ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a : ℕ → ℝ<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))) → ∑ k ∈ Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a m, f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a : ℕ → ℝ<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∀ (n : ℕ), m ≤ n → ((∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) → ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ) → (∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))) → ∑ k ∈ Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<GOAL>X ∣ φ ↔ (constantCoeff R) φ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<GOAL>(∀ m < 1, (coeff R m) φ = 0) ↔ (coeff R 0) φ = 0
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>x y : List α<VAR>s : σ<VAR>hx : M.evalFrom s x = s<VAR>hy : y ∈ {x}∗<GOAL>M.evalFrom s y = s
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>x y : List α<VAR>s : σ<VAR>hx : M.evalFrom s x = s<VAR>hy : ∃ L, y = L.join ∧ ∀ y ∈ L, y ∈ {x}<GOAL>M.evalFrom s y = s
<VAR>α : Type u<GOAL>Nonempty (Field α) ↔ IsPrimePow #α
<VAR>α : Type u<GOAL>Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>x : α<GOAL>findMax' x t.dual = t.findMin' x
<VAR>α : Type u_1<VAR>s : Multiset (Multiset α)<GOAL>∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun s a => a ∈ s) s a
<VAR>z : ℂ<GOAL>z.re ^ 2 ≤ normSq z
<VAR>z : ℂ<GOAL>z.re ^ 2 ≤ z.re ^ 2 + z.im * z.im
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>x : ↥(LinearMap.ker f)<GOAL>f ((LinearMap.ker f).subtype x) = 0
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x ≠ 0 ∨ 1 ≤ p<GOAL>HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x ≠ 0 ∨ 1 ≤ p<GOAL>f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>hurwitzZetaOdd a (-2 * ↑n - 1) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>p : α → Prop<VAR>D : DecidablePred p<VAR>f : α →₀ M<GOAL>(subtypeDomain p f).support = Finset.subtype p f.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : (i : ι) → DecidableEq (α i)<VAR>inst✝² : (i : ι) → PartialOrder (α i)<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card - 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>k : ℕ<GOAL>‖z ^ (k + 1)‖ = ‖z‖ ^ (k + 1)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>k : ℕ<GOAL>‖z ^ k‖ * ‖z‖ = ‖z‖ ^ k * ‖z‖
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<GOAL>b ∈ map f K → ∀ (y : F), (adjoint f) y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<GOAL>∀ (x : ℕ → F), (∀ (n : ℕ), ∃ x_1 ∈ K, f x_1 = x n) → Tendsto x atTop (nhds b) → ∀ (y : F), (∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ) → 0 ≤ ⟪y, b⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>seq : ℕ → F<VAR>hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n<VAR>htends : Tendsto seq atTop (nhds b)<VAR>y : F<VAR>hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ<GOAL>0 ≤ ⟪y, b⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>seq : ℕ → F<VAR>hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n<VAR>htends : Tendsto seq atTop (nhds b)<VAR>y : F<VAR>hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ<GOAL>∀ (n : ℕ), 0 ≤ ⟪y, seq n⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>seq : ℕ → F<VAR>hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n<VAR>htends : Tendsto seq atTop (nhds b)<VAR>y : F<VAR>hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ<VAR>n : ℕ<VAR>w✝ : E<VAR>h : w✝ ∈ K<VAR>hseq : f w✝ = seq n<GOAL>0 ≤ ⟪y, seq n⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : ∀ (y : F), (adjoint f) y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ<GOAL>b ∈ map f K
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<GOAL>∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<GOAL>∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<GOAL>∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<GOAL>(adjoint f) y ∈ K.dual
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<GOAL>∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<VAR>x : E<VAR>hxK : x ∈ K<GOAL>f x ∈ C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<VAR>x : E<VAR>hxK : x ∈ K<GOAL>f x ∈ ↑(PointedCone.map ↑f ↑K).closure
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<VAR>x : E<VAR>hxK : x ∈ K<GOAL>f x ∈ ↑↑(PointedCone.map ↑f ↑K)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>h : b ∉ map f K<VAR>C : ConvexCone ℝ F := ↑↑(map f K)<VAR>y : F<VAR>hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ<VAR>hyb : ⟪y, b⟫_ℝ < 0<VAR>x : E<VAR>hxK : x ∈ K<GOAL>∃ x_1 ∈ ↑↑K, f x_1 = f x
<VAR>σ : Type u<VAR>R✝ : Type v<VAR>inst✝² : CommSemiring R✝<VAR>p✝ m : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<GOAL>Finsupp.mapRange ⇑f ⋯ p = (map f) p
<VAR>σ : Type u<VAR>R✝ : Type v<VAR>inst✝² : CommSemiring R✝<VAR>p✝ m : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<GOAL>∑ x ∈ p.support, Finsupp.mapRange ⇑f ⋯ ((monomial x) (coeff x p)) = ∑ x ∈ p.support, (map f) ((monomial x) (coeff x p))