ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).inv = CategoryTheory.ComposableArrows.homMk₅ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv app₅.inv ⋯ ⋯ ⋯ ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).hom = CategoryTheory.ComposableArrows.homMk₅ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom app₅.hom w₀ w₁ w₂ w₃ w₄
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<VAR>h₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯<VAR>h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯<VAR>h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯<VAR>h₃ : f.obj' 3 ⋯ = g.obj' 3 ⋯<VAR>h₄ : f.obj' 4 ⋯ = g.obj' 4 ⋯<VAR>h₅ : f.obj' 5 ⋯ = g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₂ : f.map' 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (g.map' 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₃ : f.map' 3 4 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (g.map' 3 4 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₄ : f.map' 4 5 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₄) (CategoryTheory.CategoryStruct.comp (g.map' 4 5 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.ComposableArrows C 5<GOAL>∃ X₀ X₁ X₂ X₃ X₄ X₅ f₀ f₁ f₂ f₃ f₄, X = CategoryTheory.ComposableArrows.mk₅ f₀ f₁ f₂ f₃ f₄
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>obj : Fin (n + 1) → C<VAR>mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ<GOAL>∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = CategoryTheory.CategoryStruct.comp (e ⟨i, ⋯⟩).inv (CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (e ⟨i + 1, ⋯⟩).hom)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>obj : Fin (n + 1) → C<VAR>mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ<VAR>i : Fin (n + 1)<GOAL>(CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).obj i = obj i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>obj : Fin (n + 1) → C<VAR>mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ<VAR>i : ℕ<VAR>hi : i < n := by valid<GOAL>(CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) ⋯ hi = mapSucc ⟨i, hi⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>obj : Fin (n + 1) → C<VAR>mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ<VAR>i : ℕ<VAR>hi : i < n := by valid<GOAL>(CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).arrow i hi = CategoryTheory.ComposableArrows.mk₁ (mapSucc ⟨i, hi⟩)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ<GOAL>∀ (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X).obj X_1 = Opposite.op ((Opposite.unop X).obj X_1.rev)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<GOAL>∀ {X Y : CategoryTheory.ComposableArrows Cᵒᵖ n} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.opEquivalence C n).inverse.map f = (CategoryTheory.whiskerLeft (⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor) (CategoryTheory.NatTrans.leftOp f)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ<GOAL>(CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor) (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp (Opposite.unop X)).rightOpLeftOpIso.inv).op ((CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun F => (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc F).symm) ⋯) (CategoryTheory.NatIso.ofComponents (fun F => ((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.invFunIdAssoc F) ⋯)).hom.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ<GOAL>∀ {X_1 Y : Fin (n + 1)} (f : X_1 ⟶ Y), ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X).map f = ((Opposite.unop X).map (⋯.functor.map (CategoryTheory.homOfLE ⋯))).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : CategoryTheory.ComposableArrows Cᵒᵖ n<GOAL>(CategoryTheory.ComposableArrows.opEquivalence C n).inverse.obj X = Opposite.op ((⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor).comp (CategoryTheory.Functor.leftOp X))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : CategoryTheory.ComposableArrows Cᵒᵖ n<GOAL>∀ (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.hom.app X).app X_1 = X.map (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counitInv.app (Opposite.op X_1)).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ<GOAL>(CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun F => (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc F).symm) ⋯) (CategoryTheory.NatIso.ofComponents (fun F => ((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.invFunIdAssoc F) ⋯)).inv.app (Opposite.unop X)).op (CategoryTheory.whiskerLeft (⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor) (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp (Opposite.unop X)).rightOpLeftOpIso.hom).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<GOAL>∀ {X Y : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ} (f : X ⟶ Y) (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.map f).app X_1 = (f.unop.app X_1.rev).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>X : CategoryTheory.ComposableArrows Cᵒᵖ n<GOAL>∀ (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.inv.app X).app X_1 = X.map (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counit.app (Opposite.op X_1)).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>n : ℕ<GOAL>∀ {X Y : CategoryTheory.Functor (Fin (n + 1)) C} (α : X ⟶ Y) (X_1 : Fin (n + 1)), ((G.mapComposableArrows n).map α).app X_1 = G.map (α.app X_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>n : ℕ<VAR>F : CategoryTheory.Functor (Fin (n + 1)) C<GOAL>∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), ((G.mapComposableArrows n).obj F).map f = G.map (F.map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>n : ℕ<VAR>F : CategoryTheory.Functor (Fin (n + 1)) C<VAR>X : Fin (n + 1)<GOAL>((G.mapComposableArrows n).obj F).obj X = G.obj (F.obj X)
<VAR>S : Type u_2<VAR>CommRing S<VAR>w x y z : S<GOAL>Polynomial.C w * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) = { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly
<VAR>S : Type u_2<VAR>CommRing S<VAR>x y z : S<GOAL>(Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) = { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<GOAL>(∀ n > 3, P.toPoly.coeff n = 0) ∧ P.toPoly.coeff 3 = P.a ∧ P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>P.toPoly.coeff n = 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<GOAL>P.toPoly.coeff 3 = P.a
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<GOAL>P.toPoly.coeff 2 = P.b
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<GOAL>P.toPoly.coeff 1 = P.c
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<GOAL>P.toPoly.coeff 0 = P.d
<VAR>R : Type u_1<VAR>P Q : Cubic R<VAR>Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.a = Q.a
<VAR>R : Type u_1<VAR>P Q : Cubic R<VAR>Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.b = Q.b
<VAR>R : Type u_1<VAR>P Q : Cubic R<VAR>Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.c = Q.c
<VAR>R : Type u_1<VAR>P Q : Cubic R<VAR>Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.d = Q.d
<VAR>R : Type u_1<VAR>Semiring R<VAR>P Q : Cubic R<GOAL>P.toPoly = Q.toPoly ↔ P = Q
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<GOAL>P.toPoly = Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<GOAL>{ a := 0, b := b, c := c, d := d }.toPoly = Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<GOAL>P.toPoly = Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := c, d := d }.toPoly = Polynomial.C c * Polynomial.X + Polynomial.C d
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly = Polynomial.C P.d
<VAR>R : Type u_1<VAR>d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 0, d := d }.toPoly = Polynomial.C d
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d = 0<GOAL>P.toPoly = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 0, d := 0 }.toPoly = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Cubic.toPoly 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Cubic R<GOAL>P.toPoly = 0 ↔ P = 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0<GOAL>P.toPoly ≠ 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a ≠ 0<GOAL>P.toPoly ≠ 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>hb : P.b ≠ 0<GOAL>P.toPoly ≠ 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>hc : P.c ≠ 0<GOAL>P.toPoly ≠ 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>hd : P.d ≠ 0<GOAL>P.toPoly ≠ 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a ≠ 0<GOAL>P.toPoly.leadingCoeff = P.a
<VAR>R : Type u_1<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>{ a := a, b := b, c := c, d := d }.toPoly.leadingCoeff = a
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b ≠ 0<GOAL>P.toPoly.leadingCoeff = P.b
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<VAR>hb : b ≠ 0<GOAL>{ a := 0, b := b, c := c, d := d }.toPoly.leadingCoeff = b
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c ≠ 0<GOAL>P.toPoly.leadingCoeff = P.c
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<VAR>hc : c ≠ 0<GOAL>{ a := 0, b := 0, c := c, d := d }.toPoly.leadingCoeff = c
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly.leadingCoeff = P.d
<VAR>R : Type u_1<VAR>d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 0, d := d }.toPoly.leadingCoeff = d
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 1<GOAL>P.toPoly.Monic
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<GOAL>{ a := 1, b := b, c := c, d := d }.toPoly.Monic
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 1<GOAL>P.toPoly.Monic
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<GOAL>{ a := 0, b := 1, c := c, d := d }.toPoly.Monic
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 1<GOAL>P.toPoly.Monic
<VAR>R : Type u_1<VAR>d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 1, d := d }.toPoly.Monic
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d = 1<GOAL>P.toPoly.Monic
<GOAL>{ a := 0, b := 0, c := 0, d := 1 }.toPoly.Monic
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : { p // p.degree ≤ 3 }<GOAL>(Cubic.equiv.symm f).c = (↑f).coeff 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Cubic R<GOAL>↑(Cubic.equiv P) = P.toPoly
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : { p // p.degree ≤ 3 }<GOAL>(Cubic.equiv.symm f).b = (↑f).coeff 2
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : { p // p.degree ≤ 3 }<GOAL>(Cubic.equiv.symm f).a = (↑f).coeff 3
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : { p // p.degree ≤ 3 }<GOAL>(Cubic.equiv.symm f).d = (↑f).coeff 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a ≠ 0<GOAL>P.toPoly.degree = 3
<VAR>R : Type u_1<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>{ a := a, b := b, c := c, d := d }.toPoly.degree = 3
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<GOAL>P.toPoly.degree ≤ 2
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<GOAL>{ a := 0, b := b, c := c, d := d }.toPoly.degree ≤ 2
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b ≠ 0<GOAL>P.toPoly.degree = 2
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<VAR>hb : b ≠ 0<GOAL>{ a := 0, b := b, c := c, d := d }.toPoly.degree = 2
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<GOAL>P.toPoly.degree ≤ 1
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := c, d := d }.toPoly.degree ≤ 1
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c ≠ 0<GOAL>P.toPoly.degree = 1
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<VAR>hc : c ≠ 0<GOAL>{ a := 0, b := 0, c := c, d := d }.toPoly.degree = 1
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly.degree ≤ 0
<VAR>R : Type u_1<VAR>d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 0, d := d }.toPoly.degree ≤ 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d ≠ 0<GOAL>P.toPoly.degree = 0
<VAR>R : Type u_1<VAR>d : R<VAR>Semiring R<VAR>hd : d ≠ 0<GOAL>{ a := 0, b := 0, c := 0, d := d }.toPoly.degree = 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d = 0<GOAL>P.toPoly.degree = ⊥
<VAR>R : Type u_1<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 0, d := 0 }.toPoly.degree = ⊥
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(Cubic.toPoly 0).degree = ⊥
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a ≠ 0<GOAL>P.toPoly.natDegree = 3
<VAR>R : Type u_1<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>{ a := a, b := b, c := c, d := d }.toPoly.natDegree = 3
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<GOAL>P.toPoly.natDegree ≤ 2
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<GOAL>{ a := 0, b := b, c := c, d := d }.toPoly.natDegree ≤ 2
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b ≠ 0<GOAL>P.toPoly.natDegree = 2
<VAR>R : Type u_1<VAR>b c d : R<VAR>Semiring R<VAR>hb : b ≠ 0<GOAL>{ a := 0, b := b, c := c, d := d }.toPoly.natDegree = 2
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<GOAL>P.toPoly.natDegree ≤ 1
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := c, d := d }.toPoly.natDegree ≤ 1
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c ≠ 0<GOAL>P.toPoly.natDegree = 1
<VAR>R : Type u_1<VAR>c d : R<VAR>Semiring R<VAR>hc : c ≠ 0<GOAL>{ a := 0, b := 0, c := c, d := d }.toPoly.natDegree = 1
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly.natDegree = 0
<VAR>R : Type u_1<VAR>d : R<VAR>Semiring R<GOAL>{ a := 0, b := 0, c := 0, d := d }.toPoly.natDegree = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(Cubic.toPoly 0).natDegree = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Cubic R<VAR>Semiring R<VAR>Semiring S<VAR>φ : R →+* S<GOAL>(Cubic.map φ P).toPoly = Polynomial.map φ P.toPoly
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Cubic R<VAR>CommRing R<VAR>CommRing S<VAR>φ : R →+* S<VAR>IsDomain S<GOAL>(Cubic.map φ P).roots = (Polynomial.map φ P.toPoly).roots
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>CommRing R<VAR>IsDomain R<VAR>h0 : P.toPoly ≠ 0<VAR>x : R<GOAL>x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
<VAR>R : Type u_1<VAR>P : Cubic R<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableEq R<GOAL>P.roots.toFinset.card ≤ 3
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>ha : P.a ≠ 0<GOAL>Polynomial.Splits φ P.toPoly ↔ Multiset.card (Cubic.map φ P).roots = 3
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>ha : P.a ≠ 0<GOAL>Polynomial.Splits φ P.toPoly ↔ ∃ x y z, (Cubic.map φ P).roots = {x, y, z}
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>(Cubic.map φ P).toPoly = Polynomial.C (φ P.a) * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z)
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>Cubic.map φ P = { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>φ P.b = φ P.a * -(x + y + z)
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>φ P.c = φ P.a * (x * y + x * z + y * z)
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>φ P.d = φ P.a * -(x * y * z)
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<GOAL>P.disc ≠ 0 ↔ (Cubic.map φ P).roots.Nodup
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>Field F<VAR>Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>DecidableEq K<VAR>ha : P.a ≠ 0<VAR>h3 : (Cubic.map φ P).roots = {x, y, z}<VAR>hd : P.disc ≠ 0<GOAL>(Cubic.map φ P).roots.toFinset.card = 3
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>ModuleCat.of R ↑X.toModuleCat = X.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>(CoalgebraCat.of R X).isModule = inst✝
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>(CoalgebraCat.of R X).isAddCommGroup = inst✝
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>(CoalgebraCat.of R X).instCoalgebra = inferInstance
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>↑(CoalgebraCat.of R X).toModuleCat = X
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>Coalgebra.comul = Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>Coalgebra.counit = Coalgebra.counit
<VAR>R : Type u<VAR>CommRing R<VAR>V W : CoalgebraCat R<GOAL>Function.Injective CoalgebraCat.Hom.toCoalgHom
<VAR>R : Type u<VAR>CommRing R<VAR>M N : CoalgebraCat R<VAR>f g : M ⟶ N<VAR>h : f.toCoalgHom = g.toCoalgHom<GOAL>f = g
<VAR>R : Type u<VAR>CommRing R<VAR>M N U : CoalgebraCat R<VAR>f : M ⟶ N<VAR>g : N ⟶ U<GOAL>(f ≫ g).toCoalgHom = g.toCoalgHom.comp f.toCoalgHom
<VAR>R : Type u<VAR>CommRing R<VAR>M : CoalgebraCat R<GOAL>(𝟙 M).toCoalgHom = CoalgHom.id R ↑M.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>(CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : CoalgebraCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).map f = ↑f.toCoalgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>Coalgebra R X<VAR>Coalgebra R Y<VAR>e : X ≃ₗc[R] Y<GOAL>e.toCoalgebraCatIso.inv.toCoalgHom = ↑e.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>Coalgebra R X<VAR>Coalgebra R Y<VAR>e : X ≃ₗc[R] Y<GOAL>e.toCoalgebraCatIso.hom.toCoalgHom = ↑e
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Coalgebra R X<GOAL>(CoalgEquiv.refl R X).toCoalgebraCatIso = CategoryTheory.Iso.refl (CoalgebraCat.of R X)
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>Coalgebra R X<VAR>Coalgebra R Y<VAR>e : X ≃ₗc[R] Y<GOAL>e.symm.toCoalgebraCatIso = e.toCoalgebraCatIso.symm