ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval r) (p • q) = Polynomial.eval r p • (eval r) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval r) (p • 0) = Polynomial.eval r p • (eval r) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>∀ (f g : PolynomialModule R M), (eval r) (p • f) = Polynomial.eval r p • (eval r) f → (eval r) (p • g) = Polynomial.eval r p • (eval r) g → (eval r) (p • (f + g)) = Polynomial.eval r p • (eval r) (f + g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>∀ (a : ℕ) (b : M), (eval r) (p • (single R a) b) = Polynomial.eval r p • (eval r) ((single R a) b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<VAR>i : ℕ<VAR>m : M<GOAL>(eval r) (p • (single R i) m) = Polynomial.eval r p • (eval r) ((single R i) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>q : PolynomialModule R M<VAR>r : R<VAR>i : ℕ<VAR>m : M<VAR>p✝ q✝ : R[X]<VAR>e₁ : (eval r) (p✝ • (single R i) m) = Polynomial.eval r p✝ • (eval r) ((single R i) m)<VAR>e₂ : (eval r) (q✝ • (single R i) m) = Polynomial.eval r q✝ • (eval r) ((single R i) m)<GOAL>(eval r) ((p✝ + q✝) • (single R i) m) = Polynomial.eval r (p✝ + q✝) • (eval r) ((single R i) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>q : PolynomialModule R M<VAR>r : R<VAR>i : ℕ<VAR>m : M<VAR>n✝ : ℕ<VAR>a✝ : R<GOAL>(eval r) ((monomial n✝) a✝ • (single R i) m) = Polynomial.eval r ((monomial n✝) a✝) • (eval r) ((single R i) m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<GOAL>s.chainHeight = ⨆ i ∈ s, (s ∩ Ici i).chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<GOAL>s.chainHeight ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<GOAL>⨆ i ∈ s, (s ∩ Ici i).chainHeight ≤ s.chainHeight
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>z w : ℂ<GOAL>f z = f w
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>z w : ℂ<GOAL>∀ (c : ℂ), deriv f c = 0
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>c : ℂ<GOAL>deriv f c = 0
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>c : ℂ<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : ∀ (z : ℂ), ‖f z‖ ≤ C<GOAL>deriv f c = 0
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>c : ℂ<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : ∀ (z : ℂ), ‖f z‖ ≤ C<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<GOAL>‖deriv f c‖ ≤ ε
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Monoid α<VAR>inst✝² : AddGroup β<VAR>inst✝¹ : DistribMulAction α β<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>s : Finset α<VAR>t : Finset β<GOAL>s • -t = -(s • t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Monoid α<VAR>inst✝² : AddGroup β<VAR>inst✝¹ : DistribMulAction α β<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>s : Finset α<VAR>t : Finset β<GOAL>s • image (fun x => -x) t = image (fun x => -x) (s • t)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l₃ : List α<VAR>h : l₁ <+ l₂<GOAL>l₁.diff (a :: l₃) <+ l₂.diff (a :: l₃)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hi : i < x.order<GOAL>x.coeff i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>i : Γ<VAR>hi : i < order 0<GOAL>coeff 0 i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hi : i < x.order<VAR>hx : x ≠ 0<GOAL>x.coeff i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hx : x ≠ 0<VAR>hi : x.coeff i ≠ 0<GOAL>¬i < x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hx : x ≠ 0<VAR>hi : i ∈ x.support<GOAL>¬i < x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hx : x ≠ 0<VAR>hi : i ∈ x.support<GOAL>¬i < ⋯.min ⋯
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>inst✝ : T2Space M<VAR>i : ι<VAR>x : M<GOAL>∃ t, ⇑(fs.toSmoothPartitionOfUnity i) =ᶠ[𝓝 x] ↑(fs.toFun i) * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(fs.toFun j))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<GOAL>x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝ : InvolutiveStar R<VAR>x : R<GOAL>IsSelfAdjoint (star x) ↔ IsSelfAdjoint x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ<GOAL>f ≤ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ<GOAL>0 ≤ᶠ[ae μ] g - f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s < ⊤ → 0 ≤ ∫ (x : α) in s, (g - f) x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s < ⊤ → ∫ (a : α) in s, f a ∂μ ≤ ∫ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε' : ε ≠ ⊤<GOAL>μ {x | ε ≤ f x} * ε ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε' : ε ≠ ⊤<GOAL>ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, dist (u n) (u N) < 1<GOAL>∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, dist (u n) (u N) < 1<VAR>R : NNReal := (Finset.range N).sup fun n => nndist (u n) (u N)<GOAL>∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, dist (u n) (u N) < 1<VAR>R : NNReal := (Finset.range N).sup fun n => nndist (u n) (u N)<VAR>n : ℕ<GOAL>dist (u n) (u N) < ↑R + 1
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, dist (u n) (u N) < 1<VAR>R : NNReal := (Finset.range N).sup fun n => nndist (u n) (u N)<VAR>n : ℕ<VAR>h : N ≤ n<GOAL>dist (u n) (u N) < ↑R + 1
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, dist (u n) (u N) < 1<VAR>R : NNReal := (Finset.range N).sup fun n => nndist (u n) (u N)<VAR>n : ℕ<VAR>h : n < N<GOAL>dist (u n) (u N) < ↑R + 1
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<GOAL>map LinearMap.id = AlgHom.id R' (tsze R' M)
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<GOAL>∀ (m : M), (map LinearMap.id) (inr m) = (AlgHom.id R' (tsze R' M)) (inr m)
<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>(X ^ 0 * p).smeval x = x ^ 0 * p.smeval x
<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<VAR>n : ℕ<GOAL>(X ^ (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).hom ≫ prodSnd = prod.snd
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<GOAL>prodSnd = (X.prodBinaryFan Y).snd
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<GOAL>{x | ∃ y < x, Ioo y x = ∅}.Countable
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hz : z ∈ verticalStrip 0 1<GOAL>(fun x => ‖f z‖) ≤ᶠ[𝓝[>] 0] fun ε => ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.23232, u_1} D<VAR>P : MorphismProperty C<GOAL>P.map (𝟭 C) = P.isoClosure
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.23232, u_1} D<VAR>P : MorphismProperty C<GOAL>P.map (𝟭 C) ≤ P.isoClosure
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.23232, u_1} D<VAR>P : MorphismProperty C<GOAL>P.isoClosure ≤ P.map (𝟭 C)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>J : C<GOAL>Injective J ↔ (preadditiveYonedaObj J).PreservesEpimorphisms
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>J : C<GOAL>(yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYonedaObj J).PreservesEpimorphisms
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>hbdd : BddAbove (range f)<GOAL>Tendsto f atTop (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>hbdd : BddAbove (range f)<VAR>h✝ : IsEmpty ι<GOAL>Tendsto f atTop (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>hbdd : BddAbove (range f)<VAR>h✝ : Nonempty ι<GOAL>Tendsto f atTop (𝓝 (⨆ i, f i))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>r : R<GOAL>hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>derivWithin f S x < derivWithin f S y
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<GOAL>derivativeFun 1 = 0
<VAR>x n : ℂ<GOAL>(x ^ n)⁻¹ = if x.arg = π then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n
<VAR>x n : ℂ<GOAL>(x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<GOAL>orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>f ≫ (g + h) = f ≫ g + f ≫ h
<VAR>γ : Type u<VAR>f : Listβ γ Listα.nil → WType (Listβ γ)<GOAL>ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f
<VAR>γ : Type u<VAR>f : Listβ γ Listα.nil → WType (Listβ γ)<GOAL>PEmpty.elim = f
<VAR>γ : Type u<VAR>x : γ<VAR>f : Listβ γ (Listα.cons x) → WType (Listβ γ)<GOAL>ofList γ (toList γ (mk (Listα.cons x) f)) = mk (Listα.cons x) f
<VAR>γ : Type u<VAR>x : γ<VAR>f : Listβ γ (Listα.cons x) → WType (Listβ γ)<GOAL>(fun x => f PUnit.unit) = f
<VAR>n b m : ℕ<VAR>h : 1 < b<VAR>p : b.digits m ≠ []<VAR>q : b.digits (m / b) ≠ []<VAR>hm : ¬m = 0<GOAL>(b.digits m).getLast p = (b.digits (m / b)).getLast q
<VAR>n b m : ℕ<VAR>h : 1 < b<VAR>p : b.digits m ≠ []<VAR>q : b.digits (m / b) ≠ []<VAR>hm : ¬m = 0<GOAL>(m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a x y : G<GOAL>SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>x : C(↑s, 𝕜)<GOAL>x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔ x ∈ ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>inst✝ : (i : I) → NonUnitalNormedRing (B i)<VAR>f g : (i : I) → B i<VAR>hf : Memℓp f ⊤<VAR>hg : Memℓp g ⊤<GOAL>Memℓp (f * g) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>inst✝ : (i : I) → NonUnitalNormedRing (B i)<VAR>f g : (i : I) → B i<VAR>hf : Memℓp f ⊤<VAR>hg : Memℓp g ⊤<GOAL>BddAbove (Set.range fun i => ‖(f * g) i‖)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>inst✝ : (i : I) → NonUnitalNormedRing (B i)<VAR>f g : (i : I) → B i<VAR>hf : Memℓp f ⊤<VAR>hg : Memℓp g ⊤<VAR>Cf : ℝ<VAR>hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)<VAR>Cg : ℝ<VAR>hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)<GOAL>BddAbove (Set.range fun i => ‖(f * g) i‖)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>inst✝ : (i : I) → NonUnitalNormedRing (B i)<VAR>f g : (i : I) → B i<VAR>hf : Memℓp f ⊤<VAR>hg : Memℓp g ⊤<VAR>Cf : ℝ<VAR>hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)<VAR>Cg : ℝ<VAR>hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)<VAR>i : I<GOAL>(fun i => ‖(f * g) i‖) i ≤ Cf * Cg
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).inv ≫ prod.snd = prodSnd
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x : K[X]<VAR>y : ↥K[X]⁰<GOAL>{ toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } = IsLocalization.mk' (RatFunc K) x y
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : CommSemiring S'<VAR>inst✝⁶ : Algebra S' R<VAR>inst✝⁵ : Algebra S S'<VAR>inst✝⁴ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<GOAL>RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : CommSemiring S'<VAR>inst✝⁶ : Algebra S' R<VAR>inst✝⁵ : Algebra S S'<VAR>inst✝⁴ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<GOAL>RingHom.ker f.kerSquareLift.toRingHom ≤ (RingHom.ker f.toRingHom).cotangentIdeal