ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>X : C ⥤ CommMon_ D<GOAL>∀ (X_1 : C), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.hom.app X).app X_1).hom = 𝟙 ((CommMon_.forget₂Mon_ D).obj (X.obj X_1)).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>X : C ⥤ CommMon_ D<GOAL>∀ (X_1 : C), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.inv.app X).app X_1).hom = 𝟙 (X.obj X_1).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>(CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>(CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).counitIso = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>(CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>(CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).functor = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>#R[X] = max #R ℵ₀
<VAR>R : Type u<VAR>Semiring R<GOAL>#R[X] ≤ max #R ℵ₀
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>self : CategoryTheory.RepresentablyFlat F<VAR>X : D<GOAL>CategoryTheory.IsCofiltered (CategoryTheory.StructuredArrow X F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.RepresentablyFlat (𝟭 C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasFiniteLimits C<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>CategoryTheory.RepresentablyFlat F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>CategoryTheory.RepresentablyFlat F<VAR>c : CategoryTheory.Limits.Cone K<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cone (K ⋙ F)<VAR>x : J<GOAL>CategoryTheory.PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<VAR>F : C ⥤ D<VAR>CategoryTheory.RepresentablyFlat F<VAR>K : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone K<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cone (K ⋙ F)<VAR>f₁ f₂ : s.pt ⟶ F.obj c.pt<VAR>h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j<GOAL>f₁ = f₂
<VAR>C D : Type u₁<VAR>CategoryTheory.SmallCategory C<VAR>CategoryTheory.SmallCategory D<VAR>CategoryTheory.Limits.HasFiniteLimits C<VAR>F : C ⥤ D<GOAL>CategoryTheory.RepresentablyFlat F ↔ CategoryTheory.RepresentablyFlat F.op.lan
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>A : Type u_4<VAR>a : A<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>p : R[X]<VAR>h : (Polynomial.aeval a) p = 0<VAR>h' : p ≠ 0<GOAL>Module.IsTorsion R[X] (Module.AEval R M a)
<VAR>K : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>a : A<VAR>Field K<VAR>Ring A<VAR>Algebra K A<VAR>AddCommGroup M<VAR>Module A M<VAR>Module K M<VAR>IsScalarTower K A M<VAR>FiniteDimensional K A<GOAL>Module.IsTorsion K[X] (Module.AEval K M a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>Y : D<GOAL>(E.coconeAt Y).pt = E.right.obj Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>Y : D<VAR>g : CategoryTheory.CostructuredArrow L Y<GOAL>(E.coconeAt Y).ι.app g = CategoryTheory.CategoryStruct.comp (E.hom.app g.left) (E.right.map g.hom)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>Y : D<VAR>E E' : L.LeftExtension F<VAR>φ : E ⟶ E'<GOAL>((CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).map φ).hom = φ.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>Y : D<VAR>E : L.LeftExtension F<GOAL>(CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).obj E = E.coconeAt Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>Y : D<VAR>h : E.IsPointwiseLeftKanExtensionAt Y<GOAL>L.HasPointwiseLeftKanExtensionAt F Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>X : C<VAR>h : E.IsPointwiseLeftKanExtensionAt (L.obj X)<VAR>L.Full<VAR>L.Faithful<GOAL>CategoryTheory.IsIso (E.hom.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>h : E.IsPointwiseLeftKanExtension<GOAL>L.HasPointwiseLeftKanExtension F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<GOAL>f₁ = f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>h : E.IsPointwiseLeftKanExtension<GOAL>E.right.IsLeftKanExtension E.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>h : E.IsPointwiseLeftKanExtension<GOAL>L.HasLeftKanExtension F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.LeftExtension F<VAR>h : E.IsPointwiseLeftKanExtension<VAR>L.Full<VAR>L.Faithful<GOAL>CategoryTheory.IsIso E.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>Y : D<GOAL>(E.coneAt Y).pt = E.left.obj Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>Y : D<VAR>g : CategoryTheory.StructuredArrow Y L<GOAL>(E.coneAt Y).π.app g = CategoryTheory.CategoryStruct.comp (E.left.map g.hom) (E.hom.app g.right)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>Y : D<VAR>E : L.RightExtension F<GOAL>(CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).obj E = E.coneAt Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>Y : D<VAR>E E' : L.RightExtension F<VAR>φ : E ⟶ E'<GOAL>((CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).map φ).hom = φ.left.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>Y : D<VAR>h : E.IsPointwiseRightKanExtensionAt Y<GOAL>L.HasPointwiseRightKanExtensionAt F Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>X : C<VAR>h : E.IsPointwiseRightKanExtensionAt (L.obj X)<VAR>L.Full<VAR>L.Faithful<GOAL>CategoryTheory.IsIso (E.hom.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>h : E.IsPointwiseRightKanExtension<GOAL>L.HasPointwiseRightKanExtension F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<GOAL>f₁ = f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>h : E.IsPointwiseRightKanExtension<GOAL>E.left.IsRightKanExtension E.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>h : E.IsPointwiseRightKanExtension<GOAL>L.HasRightKanExtension F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>E : L.RightExtension F<VAR>h : E.IsPointwiseRightKanExtension<VAR>L.Full<VAR>L.Faithful<GOAL>CategoryTheory.IsIso E.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasPointwiseLeftKanExtension F<VAR>Y₁ Y₂ : D<VAR>f : Y₁ ⟶ Y₂<GOAL>(L.pointwiseLeftKanExtension F).map f = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj L Y₁).comp F) { pt := CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F), ι := { app := fun g => CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F) ((CategoryTheory.CostructuredArrow.map f).obj g), naturality := ⋯ } }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasPointwiseLeftKanExtension F<VAR>Y : D<GOAL>(L.pointwiseLeftKanExtension F).obj Y = CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasPointwiseLeftKanExtension F<VAR>X : C<GOAL>(L.pointwiseLeftKanExtensionUnit F).app X = CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L (L.obj X)).comp F) (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasPointwiseRightKanExtension F<VAR>Y₁ Y₂ : D<VAR>f : Y₁ ⟶ Y₂<GOAL>(L.pointwiseRightKanExtension F).map f = CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y₂ L).comp F) { pt := CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F), π := { app := fun g => CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F) ((CategoryTheory.StructuredArrow.map f).obj g), naturality := ⋯ } }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasPointwiseRightKanExtension F<VAR>Y : D<GOAL>(L.pointwiseRightKanExtension F).obj Y = CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasPointwiseRightKanExtension F<VAR>X : C<GOAL>(L.pointwiseRightKanExtensionCounit F).app X = CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj (L.obj X) L).comp F) (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>f : Polynomial R<GOAL>(Polynomial.taylor r) f = f.comp (Polynomial.X + Polynomial.C r)
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>(Polynomial.taylor r) Polynomial.X = Polynomial.X + Polynomial.C r
<VAR>R : Type u_1<VAR>Semiring R<VAR>r x : R<GOAL>(Polynomial.taylor r) (Polynomial.C x) = Polynomial.C x
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.taylor 0 = LinearMap.id
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>(Polynomial.taylor 0) f = f
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>(Polynomial.taylor r) 1 = Polynomial.C 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>i : ℕ<VAR>k : R<GOAL>(Polynomial.taylor r) ((Polynomial.monomial i) k) = Polynomial.C k * (Polynomial.X + Polynomial.C r) ^ i
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>f : Polynomial R<VAR>n : ℕ<GOAL>((Polynomial.taylor r) f).coeff n = Polynomial.eval r ((Polynomial.hasseDeriv n) f)
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>f : Polynomial R<GOAL>((Polynomial.taylor r) f).coeff 0 = Polynomial.eval r f
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>f : Polynomial R<GOAL>((Polynomial.taylor r) f).coeff 1 = Polynomial.eval r (Polynomial.derivative f)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>r : R<GOAL>((Polynomial.taylor r) p).natDegree = p.natDegree
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>r : R<VAR>p q : Polynomial R<GOAL>(Polynomial.taylor r) (p * q) = (Polynomial.taylor r) p * (Polynomial.taylor r) q
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>r : R<VAR>a : Polynomial R<GOAL>(Polynomial.taylorAlgHom r) a = (Polynomial.taylor r) a
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>f : Polynomial R<VAR>r s : R<GOAL>(Polynomial.taylor r) ((Polynomial.taylor s) f) = (Polynomial.taylor (r + s)) f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>r : R<VAR>f : Polynomial R<VAR>s : R<GOAL>Polynomial.eval s ((Polynomial.taylor r) f) = Polynomial.eval (s + r) f
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>f : Polynomial R<VAR>s : R<GOAL>Polynomial.eval (s - r) ((Polynomial.taylor r) f) = Polynomial.eval s f
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<GOAL>Function.Injective ⇑(Polynomial.taylor r)
<VAR>R : Type u_2<VAR>CommRing R<VAR>f : Polynomial R<VAR>r : R<VAR>h : ∀ (k : ℕ), Polynomial.eval r ((Polynomial.hasseDeriv k) f) = 0<GOAL>f = 0
<VAR>R : Type u_2<VAR>CommRing R<VAR>f : Polynomial R<VAR>r : R<GOAL>(((Polynomial.taylor r) f).sum fun i a => Polynomial.C a * (Polynomial.X - Polynomial.C r) ^ i) = f
<VAR>R : Type u<VAR>Semiring R<GOAL>WellFounded fun p q => p.trailingDegree < q.trailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.TrailingMonic ↔ p.trailingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.TrailingMonic<GOAL>p.trailingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.trailingDegree 0 = ⊤
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.trailingCoeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.natTrailingDegree 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.trailingDegree = ⊤ ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>p.trailingDegree = ↑p.natTrailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>p.trailingDegree = ↑n ↔ p.natTrailingDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>p.trailingDegree = ↑n ↔ p.natTrailingDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.trailingDegree = ↑n<GOAL>p.natTrailingDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>↑p.natTrailingDegree ≤ p.trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>q : S[X]<VAR>h : p.trailingDegree = q.trailingDegree<GOAL>p.natTrailingDegree = q.natTrailingDegree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>p.trailingDegree ≤ ↑n
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>p.natTrailingDegree ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.coeff p.natTrailingDegree = 0 ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.coeff p.natTrailingDegree ≠ 0 ↔ p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.trailingDegree = 0 ↔ p.coeff 0 ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natTrailingDegree ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.trailingDegree ≠ 0 ↔ p.coeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : q.coeff p.natTrailingDegree ≠ 0<GOAL>q.trailingDegree ≤ p.trailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>p.natTrailingDegree ≠ n → p.trailingDegree ≠ ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<VAR>H : ↑n ≤ p.trailingDegree<GOAL>n ≤ p.natTrailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hq : q ≠ 0<VAR>hpq : p.trailingDegree ≤ q.trailingDegree<GOAL>p.natTrailingDegree ≤ q.natTrailingDegree
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>((Polynomial.monomial n) a).trailingDegree = ↑n
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>((Polynomial.monomial n) a).natTrailingDegree = n
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<GOAL>((Polynomial.monomial n) a).natTrailingDegree ≤ n
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<GOAL>↑n ≤ ((Polynomial.monomial n) a).trailingDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a).trailingDegree = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>0 ≤ (Polynomial.C a).trailingDegree
<VAR>R : Type u<VAR>Semiring R<GOAL>0 ≤ Polynomial.trailingDegree 1
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).natTrailingDegree = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.natTrailingDegree 1 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(↑n).natTrailingDegree = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ n).trailingDegree = ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>↑n ≤ (Polynomial.C a * Polynomial.X ^ n).trailingDegree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : ↑n < p.trailingDegree<GOAL>p.coeff n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : n < p.natTrailingDegree<GOAL>p.coeff n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : 0 < ↑p.natTrailingDegree<GOAL>p.coeff (p.natTrailingDegree - 1) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>↑n ≤ (Polynomial.X ^ n).trailingDegree
<VAR>R : Type u<VAR>Semiring R<GOAL>1 ≤ Polynomial.X.trailingDegree
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.natTrailingDegree ≤ 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.trailingCoeff = 0 ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.trailingCoeff ≠ 0 ↔ p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p ≠ 0 → p.natTrailingDegree ∈ p.support
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : ℕ<GOAL>a ∈ p.support → p.natTrailingDegree ≤ a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p ≠ 0<GOAL>p.natTrailingDegree = p.support.min' ⋯
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>hn : ∀ m < n, p.coeff m = 0<GOAL>n ≤ p.natTrailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natTrailingDegree ≤ p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>n : ℕ<GOAL>(p * Polynomial.X ^ n).natTrailingDegree = p.natTrailingDegree + n
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p * q ≠ 0<GOAL>p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<GOAL>(p * q).trailingDegree = p.trailingDegree + q.trailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<GOAL>(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>NoZeroDivisors R<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree