ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>CategoryTheory.Category.{u_9, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>G.IsEquivalence<VAR>e : L.comp G ≅ L'<VAR>F : CategoryTheory.Functor C H<GOAL>L'.HasRightKanExtension F ↔ L.HasRightKanExtension F
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_7, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>CategoryTheory.Category.{u_9, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>G.IsEquivalence<VAR>e : L.comp G ≅ L'<VAR>F : CategoryTheory.Functor C H<VAR>F' : CategoryTheory.Functor D' H<VAR>α : F ⟶ L'.comp F'<GOAL>F'.IsLeftKanExtension α ↔ (G.comp F').IsLeftKanExtension (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.inv F') (L.associator G F').hom))
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_7, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>CategoryTheory.Category.{u_9, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>G.IsEquivalence<VAR>e : L.comp G ≅ L'<VAR>F : CategoryTheory.Functor C H<VAR>F' : CategoryTheory.Functor D' H<VAR>α : L'.comp F' ⟶ F<GOAL>F'.IsRightKanExtension α ↔ (G.comp F').IsRightKanExtension (CategoryTheory.CategoryStruct.comp (L.associator G F').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.hom F') α))
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Functor.LeftExtension.precomp L F G).map φ).left = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)<GOAL>((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).left = X.left
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)<GOAL>((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).right = X.right
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)<GOAL>∀ (X_1 : C'), ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).hom.app X_1 = X.hom.app (G.obj X_1)
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Functor.LeftExtension.precomp L F G).map φ).right = φ.right
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)<GOAL>((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).left = X.left
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Functor.RightExtension.precomp L F G).map φ).left = φ.left
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)<GOAL>∀ (X_1 : C'), ((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).hom.app X_1 = X.hom.app (G.obj X_1)
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Functor.RightExtension.precomp L F G).map φ).right = CategoryTheory.CategoryStruct.id X.right
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_2} C'<VAR>CategoryTheory.Category.{u_9, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>G : CategoryTheory.Functor C' C<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)<GOAL>((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).right = X.right
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_10, u_2} C'<VAR>CategoryTheory.Category.{u_7, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>F' : CategoryTheory.Functor D H<VAR>G : CategoryTheory.Functor C' C<VAR>G.IsEquivalence<VAR>α : F ⟶ L.comp F'<GOAL>F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G α) (G.associator L F').inv)
<VAR>C : Type u_1<VAR>C' : Type u_2<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_10, u_2} C'<VAR>CategoryTheory.Category.{u_7, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>F' : CategoryTheory.Functor D H<VAR>G : CategoryTheory.Functor C' C<VAR>G.IsEquivalence<VAR>α : L.comp F' ⟶ F<GOAL>F'.IsRightKanExtension α ↔ F'.IsRightKanExtension (CategoryTheory.CategoryStruct.comp (G.associator L F').hom (CategoryTheory.whiskerLeft G α))
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>L L' : CategoryTheory.Functor C D<VAR>iso₁ : L ≅ L'<VAR>F : CategoryTheory.Functor C H<GOAL>L.HasRightKanExtension F ↔ L'.HasRightKanExtension F
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>L L' : CategoryTheory.Functor C D<VAR>iso₁ : L ≅ L'<VAR>F : CategoryTheory.Functor C H<GOAL>L.HasLeftKanExtension F ↔ L'.HasLeftKanExtension F
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F F' : CategoryTheory.Functor C H<VAR>iso₂ : F ≅ F'<GOAL>L.HasRightKanExtension F ↔ L.HasRightKanExtension F'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F F' : CategoryTheory.Functor C H<VAR>iso₂ : F ≅ F'<GOAL>L.HasLeftKanExtension F ↔ L.HasLeftKanExtension F'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F₁ F₂ : CategoryTheory.Functor C H<VAR>F₁' F₂' : CategoryTheory.Functor D H<VAR>α₁ : F₁ ⟶ L.comp F₁'<VAR>α₂ : F₂ ⟶ L.comp F₂'<VAR>e : F₁ ≅ F₂<VAR>e' : F₁' ≅ F₂'<VAR>h : CategoryTheory.CategoryStruct.comp α₁ (CategoryTheory.whiskerLeft L e'.hom) = CategoryTheory.CategoryStruct.comp e.hom α₂<GOAL>F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F₁ F₂ : CategoryTheory.Functor C H<VAR>F₁' F₂' : CategoryTheory.Functor D H<VAR>α₁ : L.comp F₁' ⟶ F₁<VAR>α₂ : L.comp F₂' ⟶ F₂<VAR>e : F₁ ≅ F₂<VAR>e' : F₁' ≅ F₂'<VAR>h : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e'.hom) α₂ = CategoryTheory.CategoryStruct.comp α₁ e.hom<GOAL>F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Zero β<VAR>LE β<VAR>FunLike F α β<VAR>self : NonnegHomClass F α β<VAR>f : F<VAR>a : α<GOAL>0 ≤ f a
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Add α<VAR>Add β<VAR>LE β<VAR>FunLike F α β<VAR>self : SubadditiveHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a + b) ≤ f a + f b
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Mul α<VAR>Mul β<VAR>LE β<VAR>FunLike F α β<VAR>self : SubmultiplicativeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a * b) ≤ f a * f b
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Mul α<VAR>Add β<VAR>LE β<VAR>FunLike F α β<VAR>self : MulLEAddHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a * b) ≤ f a + f b
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Add α<VAR>LinearOrder β<VAR>FunLike F α β<VAR>self : NonarchimedeanHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a + b) ≤ max (f a) (f b)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>CommSemigroup β<VAR>LE β<VAR>SubmultiplicativeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ≤ f b * f (a / b)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>AddCommSemigroup β<VAR>LE β<VAR>SubadditiveHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ≤ f b + f (a - b)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>AddCommSemigroup β<VAR>LE β<VAR>MulLEAddHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ≤ f b + f (a / b)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>CommSemigroup β<VAR>LE β<VAR>SubmultiplicativeHomClass F α β<VAR>f : F<VAR>a b c : α<GOAL>f (a / c) ≤ f (a / b) * f (b / c)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>AddCommSemigroup β<VAR>LE β<VAR>SubadditiveHomClass F α β<VAR>f : F<VAR>a b c : α<GOAL>f (a - c) ≤ f (a - b) + f (b - c)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>AddCommSemigroup β<VAR>LE β<VAR>MulLEAddHomClass F α β<VAR>f : F<VAR>a b c : α<GOAL>f (a / c) ≤ f (a / b) + f (b / c)
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>FunLike F α β<VAR>self : AddGroupSeminormClass F α β<VAR>f : F<GOAL>f 0 = 0
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>FunLike F α β<VAR>self : AddGroupSeminormClass F α β<VAR>f : F<VAR>a : α<GOAL>f (-a) = f a
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>FunLike F α β<VAR>self : GroupSeminormClass F α β<VAR>f : F<GOAL>f 1 = 0
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>FunLike F α β<VAR>self : GroupSeminormClass F α β<VAR>f : F<VAR>a : α<GOAL>f a⁻¹ = f a
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>FunLike F α β<VAR>self : AddGroupNormClass F α β<VAR>f : F<VAR>a : α<GOAL>f a = 0 → a = 0
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>FunLike F α β<VAR>self : GroupNormClass F α β<VAR>f : F<VAR>a : α<GOAL>f a = 0 → a = 1
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x / y) ≤ f x + f y
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>AddGroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x - y) ≤ f x + f y
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x / y) = f (y / x)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>AddGroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x - y) = f (y - x)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f x ≤ f y + f (y / x)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>AddGroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f x ≤ f y + f (y - x)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>LinearOrderedAddCommGroup β<VAR>GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>|f x - f y| ≤ f (x / y)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>LinearOrderedAddCommGroup β<VAR>AddGroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>|f x - f y| ≤ f (x - y)
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>AddGroupNormClass F α β<VAR>f : F<VAR>x : α<GOAL>f x = 0 ↔ x = 0
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>GroupNormClass F α β<VAR>f : F<VAR>x : α<GOAL>f x = 0 ↔ x = 1
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>OrderedAddCommMonoid β<VAR>AddGroupNormClass F α β<VAR>f : F<VAR>x : α<GOAL>f x ≠ 0 ↔ x ≠ 0
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>OrderedAddCommMonoid β<VAR>GroupNormClass F α β<VAR>f : F<VAR>x : α<GOAL>f x ≠ 0 ↔ x ≠ 1
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>AddGroup α<VAR>LinearOrderedAddCommMonoid β<VAR>AddGroupNormClass F α β<VAR>f : F<VAR>x : α<VAR>hx : x ≠ 0<GOAL>0 < f x
<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>Group α<VAR>LinearOrderedAddCommMonoid β<VAR>GroupNormClass F α β<VAR>f : F<VAR>x : α<VAR>hx : x ≠ 1<GOAL>0 < f x
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : Type u_3<VAR>LE β<VAR>One β<VAR>v₁ : α₁ → β<VAR>v₂ : α₂ → β<GOAL>1 ≤ Sum.elim v₁ v₂ ↔ 1 ≤ v₁ ∧ 1 ≤ v₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : Type u_3<VAR>LE β<VAR>Zero β<VAR>v₁ : α₁ → β<VAR>v₂ : α₂ → β<GOAL>0 ≤ Sum.elim v₁ v₂ ↔ 0 ≤ v₁ ∧ 0 ≤ v₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : Type u_3<VAR>LE β<VAR>One β<VAR>v₁ : α₁ → β<VAR>v₂ : α₂ → β<GOAL>Sum.elim v₁ v₂ ≤ 1 ↔ v₁ ≤ 1 ∧ v₂ ≤ 1
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : Type u_3<VAR>LE β<VAR>Zero β<VAR>v₁ : α₁ → β<VAR>v₂ : α₂ → β<GOAL>Sum.elim v₁ v₂ ≤ 0 ↔ v₁ ≤ 0 ∧ v₂ ≤ 0
<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>LE α<VAR>self : ZeroLEOneClass α<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>LE α<VAR>ZeroLEOneClass α<GOAL>0 ≤ 1
<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>LE α<VAR>ZeroLEOneClass α<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<GOAL>0 < 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<VAR>f : Polynomial R<GOAL>(Polynomial.hasseDeriv k) f = f.sum fun i r => (Polynomial.monomial (i - k)) (↑(i.choose k) * r)
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<VAR>f : Polynomial R<VAR>n : ℕ<GOAL>((Polynomial.hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>(Polynomial.hasseDeriv 0) f = f
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.hasseDeriv 0 = LinearMap.id
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>(Polynomial.hasseDeriv n) p = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>(Polynomial.hasseDeriv 1) f = Polynomial.derivative f
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.hasseDeriv 1 = Polynomial.derivative
<VAR>R : Type u_1<VAR>Semiring R<VAR>k n : ℕ<VAR>r : R<GOAL>(Polynomial.hasseDeriv k) ((Polynomial.monomial n) r) = (Polynomial.monomial (n - k)) (↑(n.choose k) * r)
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<VAR>r : R<VAR>hk : 0 < k<GOAL>(Polynomial.hasseDeriv k) (Polynomial.C r) = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<VAR>hk : 0 < k<GOAL>(Polynomial.hasseDeriv k) 1 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<VAR>hk : 1 < k<GOAL>(Polynomial.hasseDeriv k) Polynomial.X = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<GOAL>⇑(k.factorial • Polynomial.hasseDeriv k) = (⇑Polynomial.derivative)^[k]
<VAR>R : Type u_1<VAR>Semiring R<VAR>k l : ℕ<GOAL>Polynomial.hasseDeriv k ∘ₗ Polynomial.hasseDeriv l = (k + l).choose k • Polynomial.hasseDeriv (k + l)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>((Polynomial.hasseDeriv n) p).natDegree ≤ p.natDegree - n
<VAR>R : Type u_1<VAR>Semiring R<VAR>NoZeroSMulDivisors ℕ R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>((Polynomial.hasseDeriv n) p).natDegree = p.natDegree - n
<VAR>R : Type u_1<VAR>Semiring R<VAR>k : ℕ<VAR>f g : Polynomial R<GOAL>(Polynomial.hasseDeriv k) (f * g) = ∑ ij ∈ Finset.antidiagonal k, (Polynomial.hasseDeriv ij.1) f * (Polynomial.hasseDeriv ij.2) g
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.Monic 0 ↔ Subsingleton R
<VAR>R : Type u<VAR>Semiring R<GOAL>¬Polynomial.Monic 0 ↔ 0 ≠ 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.Monic 0 ↔ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p = Polynomial.X ^ p.natDegree + ∑ i ∈ Finset.range p.natDegree, Polynomial.C (p.coeff i) * Polynomial.X ^ i
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hq : q.Monic<GOAL>q ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>hp : p.Monic<GOAL>(Polynomial.map f p).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>b : R<VAR>hp : b * p.leadingCoeff = 1<GOAL>(Polynomial.C b * p).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>b : R<VAR>hp : p.leadingCoeff * b = 1<GOAL>(p * Polynomial.C b).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>H1 : p.degree ≤ ↑n<VAR>H2 : p.coeff n = 1<GOAL>p.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>H : p.degree ≤ ↑n<GOAL>(Polynomial.X ^ (n + 1) + p).Monic
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(Polynomial.X ^ n + Polynomial.C a).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>(Polynomial.X + Polynomial.C x).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<GOAL>(p * q).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>n : ℕ<GOAL>(p ^ n).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hpq : q.degree < p.degree<GOAL>(p + q).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>hpq : p.degree < q.degree<GOAL>(p + q).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hpq : (p * q).Monic<GOAL>q.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>hpq : (p * q).Monic<GOAL>p.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p.natDegree = 0 ↔ p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p.degree ≤ 0 ↔ p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<GOAL>(p * q).degree = (q * p).degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q ≠ 0<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<GOAL>(p * q).natDegree = (q * p).natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>h0 : q ≠ 0<VAR>hl : q.natDegree < p.natDegree<GOAL>¬p ∣ q
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>h0 : q ≠ 0<VAR>hl : q.degree < p.degree<GOAL>¬p ∣ q
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<GOAL>(p * q).nextCoeff = p.nextCoeff + q.nextCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>n : ℕ<GOAL>(p ^ n).nextCoeff = n • p.nextCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>S : Type u_1<VAR>Semiring S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>map_eq : Polynomial.map f p = 1<GOAL>p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>n : ℕ<GOAL>(p ^ n).natDegree = n * p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℕ<VAR>r : R<GOAL>((Polynomial.X + Polynomial.C r) ^ n).natDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hm : p.Monic<VAR>hpu : IsUnit p<GOAL>p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hm : p.Monic<GOAL>IsUnit p ↔ p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>hpq : Associated p q<GOAL>p = q
<VAR>R : Type u<VAR>ι : Type y<VAR>CommSemiring R<VAR>t : Multiset ι<VAR>f : ι → R[X]<VAR>ht : ∀ i ∈ t, (f i).Monic<GOAL>(Multiset.map f t).prod.Monic
<VAR>R : Type u<VAR>ι : Type y<VAR>CommSemiring R<VAR>s : Finset ι<VAR>f : ι → R[X]<VAR>hs : ∀ i ∈ s, (f i).Monic<GOAL>(∏ i ∈ s, f i).Monic
<VAR>R : Type u<VAR>ι : Type y<VAR>CommSemiring R<VAR>t : Multiset ι<VAR>f : ι → R[X]<VAR>h : ∀ i ∈ t, (f i).Monic<GOAL>(Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
<VAR>R : Type u<VAR>ι : Type y<VAR>CommSemiring R<VAR>s : Finset ι<VAR>f : ι → R[X]<VAR>h : ∀ i ∈ s, (f i).Monic<GOAL>(∏ i ∈ s, f i).nextCoeff = ∑ i ∈ s, (f i).nextCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>Nontrivial S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>f : R →+* S<GOAL>(Polynomial.map f P).natDegree = P.natDegree