ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<VAR>hs : s.Nonempty<GOAL>⊤ ∈ s
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<VAR>hs : s.Nonempty<VAR>this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'<GOAL>⊤ ∈ s
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<VAR>hs : s.Nonempty<VAR>this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'<VAR>_i5 : IsNoetherian R ↥L'<GOAL>⊤ ∈ s
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<VAR>hs : s.Nonempty<VAR>this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'<VAR>_i5 : IsNoetherian R ↥L'<VAR>K : LieSubalgebra R ↥L'<VAR>hK₁ : K ∈ s<VAR>hK₂ : ∀ x ∈ s, ¬x > K<GOAL>⊤ ∈ s
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<VAR>hs : s.Nonempty<VAR>this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'<VAR>_i5 : IsNoetherian R ↥L'<VAR>K : LieSubalgebra R ↥L'<VAR>hK₁ : K ∈ s<VAR>hK₂ : ∀ x ∈ s, ¬x > K<VAR>hK₃ : K = ⊤<GOAL>⊤ ∈ s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι<GOAL>(fun i => EquivLike.coe e.symm (EuclideanSpace.single i 1)) = fun i => EquivLike.coe e.symm (EuclideanSpace.single i 1)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι<VAR>x✝ : ι<GOAL>EquivLike.coe e.symm (EuclideanSpace.single x✝ 1) = EquivLike.coe e.symm (EuclideanSpace.single x✝ 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun z => z ^ p * (1 + ε z)) =Θ[atTop] fun z => z ^ (p - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : c.IsLimit<GOAL>a < b * c ↔ ∃ c' < c, a < b * c'
<VAR>x x₁ x₂ x₃ x' y y₁✝ y₂✝ y₃ y' y₁ y₂ : PGame<VAR>i : x₂.LeftMoves<VAR>h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hl : x₁ ≤ x₂.moveLeft i<GOAL>P3 x₁ x₂ y₁ y₂
<VAR>x x₁ x₂ x₃ x' y y₁✝ y₂✝ y₃ y' y₁ y₂ : PGame<VAR>i : x₂.LeftMoves<VAR>h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hl✝ : x₁ ≤ x₂.moveLeft i<VAR>hl : x₁ < x₂.moveLeft i<GOAL>P3 x₁ x₂ y₁ y₂
<VAR>x x₁ x₂ x₃ x' y y₁✝ y₂✝ y₃ y' y₁ y₂ : PGame<VAR>i : x₂.LeftMoves<VAR>h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hl : x₁ ≤ x₂.moveLeft i<VAR>he : x₁ ≈ x₂.moveLeft i<GOAL>P3 x₁ x₂ y₁ y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<GOAL>a + b = a + b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hmo : q.Monic<VAR>a✝ : Nontrivial R<GOAL>q * p /ₘ q = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hmo : q.Monic<VAR>a✝ : Nontrivial R<GOAL>degree 0 < q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hmo : q.Monic<VAR>a✝ : Nontrivial R<GOAL>⊥ < q.degree
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>0 ≤ ∫ (x : Ω), stoppedValue f (leastGE f r i) x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>0 ≤ ∫ (x : Ω) in Set.univ, stoppedValue f (leastGE f r i) x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>0 ≤ ∫ (ω : Ω) in Set.univ, stoppedValue f (leastGE f r 0) ω ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>map f (cons a ⟨s, al⟩) = cons (f a) (map f ⟨s, al⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>↑(map f (cons a ⟨s, al⟩)) = ↑(cons (f a) (map f ⟨s, al⟩))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>p n : ℕ<VAR>inst✝² : ExpChar R p<VAR>f : R[X]<VAR>inst✝¹ : PerfectRing R p<VAR>inst✝ : DecidableEq R<GOAL>Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset = f.roots.toFinset
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : ↥(A i)<GOAL>((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) j = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>h : LineDifferentiableWithinAt 𝕜 f s x (c • v)<GOAL>LineDifferentiableWithinAt 𝕜 f s x v
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>hr : 0 ≤ r<GOAL>↑‖r‖₊ = ENNReal.ofReal r
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<GOAL>thickenedIndicatorAux δ E x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t u : Set α<VAR>h₀ : a ∈ s<VAR>h₁ : IsOpen s<VAR>h₂ : t ∩ s = u ∩ s<GOAL>𝓝[t] a = 𝓝[u] a
<VAR>d : ℤ<VAR>a : ℤ√d<GOAL>a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x < y ∨ x ≈ y ∨ y ⧏ x
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsNormalSubgroup s<VAR>a b : G<VAR>hab : a * b ∈ s<GOAL>b * a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : b.IsLimit<VAR>H : ∀ b' < b, a * b' ≤ c<GOAL>¬c < a * b
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>a b✝ x b : α<GOAL>b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>C : ℕ → Sort u_1<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>Hnext : ∀ (n : ℕ), Surjective next<GOAL>Surjective (leRecOn hnm fun {k} => next)
<VAR>u v : PrimeMultiset<GOAL>(coePNatMonoidHom (u + v)).prod = u.prod * v.prod
<VAR>u v : PrimeMultiset<GOAL>(coePNatMonoidHom u + coePNatMonoidHom v).prod = u.prod * v.prod
<VAR>n : ℕ<GOAL>(finRotate (n + 2)).cycleType = {n + 2}
<VAR>n : ℕ<GOAL>↑[n + 2] = {n + 2}
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]<VAR>z : DirectLimit G fun i j h => ⇑(f' i j h)<VAR>i : ι<VAR>x : G i<VAR>h : (of G (fun i j h => ⇑(f' i j h)) i) x = z<GOAL>Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) (C x) = C z
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]<VAR>q₁ q₂ : (DirectLimit G fun i j h => ⇑(f' i j h))[X]<VAR>x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₁<VAR>x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₂<VAR>i₁ : ι<VAR>p₁ : (G i₁)[X]<VAR>ih₁ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ = q₁<VAR>i₂ : ι<VAR>p₂ : (G i₂)[X]<VAR>ih₂ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂ = q₂<VAR>i : ι<VAR>h1 : i₁ ≤ i<VAR>h2 : i₂ ≤ i<GOAL>Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) (Polynomial.map (f' i₁ i h1) p₁ + Polynomial.map (f' i₂ i h2) p₂) = q₁ + q₂
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]<VAR>q₁ q₂ : (DirectLimit G fun i j h => ⇑(f' i j h))[X]<VAR>x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₁<VAR>x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = q₂<VAR>i₁ : ι<VAR>p₁ : (G i₁)[X]<VAR>ih₁ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ = q₁<VAR>i₂ : ι<VAR>p₂ : (G i₂)[X]<VAR>ih₂ : Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂ = q₂<VAR>i : ι<VAR>h1 : i₁ ≤ i<VAR>h2 : i₂ ≤ i<GOAL>Polynomial.map ((of G (fun i j h => ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ + Polynomial.map ((of G (fun i j h => ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ = Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i₂) p₂
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>q : (DirectLimit G fun i j h => ⇑(f' i j h))[X]<VAR>n : ℕ<VAR>z : DirectLimit G fun i j h => ⇑(f' i j h)<VAR>x✝ : ∃ i p, Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) p = C z * X ^ n<VAR>i : ι<VAR>x : G i<VAR>h : (of G (fun i j h => ⇑(f' i j h)) i) x = z<GOAL>Polynomial.map (of G (fun i j h => ⇑(f' i j h)) i) (C x * X ^ (n + 1)) = C z * X ^ (n + 1)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsClosed s<GOAL>interior (frontier s) = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsClosed s<VAR>A : frontier s = s \ interior s<GOAL>interior (frontier s) = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsClosed s<VAR>A : frontier s = s \ interior s<VAR>B : interior (frontier s) ⊆ interior s<GOAL>interior (frontier s) = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsClosed s<VAR>A : frontier s = s \ interior s<VAR>B : interior (frontier s) ⊆ interior s<VAR>C : interior (frontier s) ⊆ frontier s<GOAL>interior (frontier s) = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsClosed s<VAR>A : frontier s = s \ interior s<VAR>B : interior (frontier s) ⊆ interior s<VAR>C : interior (frontier s) ⊆ frontier s<VAR>this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)<GOAL>interior (frontier s) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : CommSemiring β<VAR>inst✝¹ : ContinuousAdd β<VAR>inst✝ : ContinuousMul β<VAR>hf : SuperpolynomialDecay l k f<VAR>p✝ p q : β[X]<VAR>hp : SuperpolynomialDecay l k fun x => eval (k x) p * f x<VAR>hq : SuperpolynomialDecay l k fun x => eval (k x) q * f x<GOAL>SuperpolynomialDecay l k fun x => eval (k x) (p + q) * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : CommSemiring β<VAR>inst✝¹ : ContinuousAdd β<VAR>inst✝ : ContinuousMul β<VAR>hf : SuperpolynomialDecay l k f<VAR>p : β[X]<VAR>n : ℕ<VAR>c : β<GOAL>SuperpolynomialDecay l k fun x => eval (k x) ((monomial n) c) * f x
<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✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n✝ m n : ℕ<VAR>hmn : m ≤ n<GOAL>x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
<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✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n m k : ℕ<VAR>hmn : m ≤ m + k<GOAL>x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
<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✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n m k : ℕ<VAR>hmn : m ≤ m + k<GOAL>k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : R[X]<GOAL>derivative (p.comp q) = derivative q * (derivative p).comp q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>q p✝ q✝ : R[X]<VAR>a✝¹ : derivative (p✝.comp q) = derivative q * (derivative p✝).comp q<VAR>a✝ : derivative (q✝.comp q) = derivative q * (derivative q✝).comp q<GOAL>derivative ((p✝ + q✝).comp q) = derivative q * (derivative (p✝ + q✝)).comp q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>q : R[X]<VAR>n✝ : ℕ<VAR>a✝ : R<GOAL>derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³¹ : AddCommMonoid M<VAR>inst✝³⁰ : AddCommMonoid N<VAR>inst✝²⁹ : CommSemiring R<VAR>inst✝²⁸ : CommSemiring S<VAR>inst✝²⁷ : Algebra R S<VAR>inst✝²⁶ : Module R M<VAR>inst✝²⁵ : Module R N<VAR>inst✝²⁴ : Module S N<VAR>inst✝²³ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h✝ : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²² : AddCommMonoid P<VAR>inst✝²¹ : Module R P<VAR>inst✝²⁰ : AddCommMonoid Q<VAR>inst✝¹⁹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁸ : CommSemiring T<VAR>inst✝¹⁷ : Algebra R T<VAR>inst✝¹⁶ : Algebra S T<VAR>inst✝¹⁵ : IsScalarTower R S T<VAR>inst✝¹⁴ : AddCommMonoid O<VAR>inst✝¹³ : Module R O<VAR>inst✝¹² : Module S O<VAR>inst✝¹¹ : Module T O<VAR>inst✝¹⁰ : IsScalarTower S T O<VAR>inst✝⁹ : IsScalarTower R S O<VAR>inst✝⁸ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring S'<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R' S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R R' S'<VAR>inst✝ : IsScalarTower R S S'<VAR>h : IsPushout R S R' S'<VAR>x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra<VAR>e : R' ⊗[R] S ≃ₗ[R'] S' := let __src := _root_.TensorProduct.comm R R' S ≪≫ₗ LinearEquiv.restrictScalars R ⋯.equiv; { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }<GOAL>IsPushout R R' S S'
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³¹ : AddCommMonoid M<VAR>inst✝³⁰ : AddCommMonoid N<VAR>inst✝²⁹ : CommSemiring R<VAR>inst✝²⁸ : CommSemiring S<VAR>inst✝²⁷ : Algebra R S<VAR>inst✝²⁶ : Module R M<VAR>inst✝²⁵ : Module R N<VAR>inst✝²⁴ : Module S N<VAR>inst✝²³ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h✝ : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²² : AddCommMonoid P<VAR>inst✝²¹ : Module R P<VAR>inst✝²⁰ : AddCommMonoid Q<VAR>inst✝¹⁹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁸ : CommSemiring T<VAR>inst✝¹⁷ : Algebra R T<VAR>inst✝¹⁶ : Algebra S T<VAR>inst✝¹⁵ : IsScalarTower R S T<VAR>inst✝¹⁴ : AddCommMonoid O<VAR>inst✝¹³ : Module R O<VAR>inst✝¹² : Module S O<VAR>inst✝¹¹ : Module T O<VAR>inst✝¹⁰ : IsScalarTower S T O<VAR>inst✝⁹ : IsScalarTower R S O<VAR>inst✝⁸ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring S'<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R' S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R R' S'<VAR>inst✝ : IsScalarTower R S S'<VAR>h : IsPushout R S R' S'<VAR>x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra<VAR>e : R' ⊗[R] S ≃ₗ[R'] S' := let __src := _root_.TensorProduct.comm R R' S ≪≫ₗ LinearEquiv.restrictScalars R ⋯.equiv; { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }<VAR>this : (toAlgHom R S S').toLinearMap = ↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1<GOAL>IsPushout R R' S S'
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³¹ : AddCommMonoid M<VAR>inst✝³⁰ : AddCommMonoid N<VAR>inst✝²⁹ : CommSemiring R<VAR>inst✝²⁸ : CommSemiring S<VAR>inst✝²⁷ : Algebra R S<VAR>inst✝²⁶ : Module R M<VAR>inst✝²⁵ : Module R N<VAR>inst✝²⁴ : Module S N<VAR>inst✝²³ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h✝ : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²² : AddCommMonoid P<VAR>inst✝²¹ : Module R P<VAR>inst✝²⁰ : AddCommMonoid Q<VAR>inst✝¹⁹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁸ : CommSemiring T<VAR>inst✝¹⁷ : Algebra R T<VAR>inst✝¹⁶ : Algebra S T<VAR>inst✝¹⁵ : IsScalarTower R S T<VAR>inst✝¹⁴ : AddCommMonoid O<VAR>inst✝¹³ : Module R O<VAR>inst✝¹² : Module S O<VAR>inst✝¹¹ : Module T O<VAR>inst✝¹⁰ : IsScalarTower S T O<VAR>inst✝⁹ : IsScalarTower R S O<VAR>inst✝⁸ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring S'<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R' S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R R' S'<VAR>inst✝ : IsScalarTower R S S'<VAR>h : IsPushout R S R' S'<VAR>x✝ : Algebra R' (S ⊗[R] R') := TensorProduct.includeRight.toAlgebra<VAR>e : R' ⊗[R] S ≃ₗ[R'] S' := let __src := _root_.TensorProduct.comm R R' S ≪≫ₗ LinearEquiv.restrictScalars R ⋯.equiv; { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }<VAR>this : (toAlgHom R S S').toLinearMap = ↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1<GOAL>IsBaseChange R' (↑R ↑e ∘ₗ (TensorProduct.mk R R' S) 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g₁ g₂ : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>const R f g₁ U hu₁ * const R g₁ g₂ U hu₂ = const R f g₂ U hu₂
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g₁ g₂ : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>f * g₁ * g₂ = f * (g₁ * g₂)
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp ^ n