ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Semiring R<VAR>P : R[X] → Prop<VAR>p : R[X]<VAR>h0 : 0 < p.degree<VAR>hC : ∀ {a : R}, a ≠ 0 → P (Polynomial.C a * Polynomial.X)<VAR>hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * Polynomial.X)<VAR>hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + Polynomial.C a)<GOAL>P p
<VAR>R : Type u<VAR>Semiring R<VAR>M : R[X] → Prop<VAR>f : R[X]<VAR>f0 : f.natDegree ≠ 0<VAR>h_C_add : ∀ {a : R} {p : R[X]}, M p → M (Polynomial.C a + p)<VAR>h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)<VAR>h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((Polynomial.monomial n) a)<GOAL>M f
<VAR>R : Type<VAR>CommRing R<VAR>IsDomain R<VAR>K : Type<VAR>Field K<VAR>Algebra R[X] K<VAR>IsFractionRing R[X] K<VAR>f : R[X]<VAR>g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>hcoprime : IsCoprime g₁ g₂<GOAL>∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
<VAR>R : Type<VAR>CommRing R<VAR>IsDomain R<VAR>K : Type<VAR>Field K<VAR>Algebra R[X] K<VAR>IsFractionRing R[X] K<VAR>f : R[X]<VAR>ι : Type u_1<VAR>g : ι → R[X]<VAR>s : Finset ι<VAR>hg : ∀ i ∈ s, (g i).Monic<VAR>hcop : (↑s).Pairwise fun i j => IsCoprime (g i) (g j)<GOAL>∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X : (i : I) → C i<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.id X i = CategoryTheory.CategoryStruct.id (X i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y Z : (i : I) → C i<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f g : X ⟶ Y<VAR>w : ∀ (i : I), f i = g i<GOAL>f = g
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i : I<VAR>f : (i : I) → C i<GOAL>(CategoryTheory.Pi.eval C i).obj f = f i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i : I<GOAL>∀ {X Y : (i : I) → C i} (α : X ⟶ Y), (CategoryTheory.Pi.eval C i).map α = α i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>h : J → I<GOAL>∀ {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J), (CategoryTheory.Pi.comap C h).map α i = α (h i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>h : J → I<VAR>f : (i : I) → C i<VAR>i : J<GOAL>(CategoryTheory.Pi.comap C h).obj f i = f (h i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X : (i : I) → C i<VAR>i : I<GOAL>(CategoryTheory.Pi.comapId I C).hom.app X i = CategoryTheory.CategoryStruct.id X i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X : (i : I) → C i<VAR>i : I<GOAL>(CategoryTheory.Pi.comapId I C).inv.app X i = CategoryTheory.CategoryStruct.id X i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>K : Type w₂<VAR>f : K → J<VAR>g : J → I<VAR>X : (i : I) → C i<VAR>b : K<GOAL>(CategoryTheory.Pi.comapComp C f g).inv.app X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>K : Type w₂<VAR>f : K → J<VAR>g : J → I<VAR>X : (i : I) → C i<VAR>b : K<GOAL>(CategoryTheory.Pi.comapComp C f g).hom.app X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>h : J → I<VAR>j : J<VAR>X : (i : I) → C i<GOAL>(CategoryTheory.Pi.comapEvalIsoEval C h j).inv.app X = CategoryTheory.CategoryStruct.id (X (h j))
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>h : J → I<VAR>j : J<VAR>X : (i : I) → C i<GOAL>(CategoryTheory.Pi.comapEvalIsoEval C h j).hom.app X = CategoryTheory.CategoryStruct.id (X (h j))
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₀<VAR>D : J → Type u₁<VAR>(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)<VAR>X : (i : I) → C i<VAR>Y Y' : (j : J) → D j<VAR>f : Y ⟶ Y'<VAR>s : I ⊕ J<GOAL>((CategoryTheory.Pi.sum C).obj X).map f s = match s with | Sum.inl i => CategoryTheory.CategoryStruct.id (X i) | Sum.inr j => f j
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₀<VAR>D : J → Type u₁<VAR>(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)<VAR>X : (i : I) → C i<VAR>Y : (j : J) → D j<VAR>s : I ⊕ J<GOAL>((CategoryTheory.Pi.sum C).obj X).obj Y s = match s with | Sum.inl i => X i | Sum.inr j => Y j
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₀<VAR>D : J → Type u₁<VAR>(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)<VAR>X X' : (i : I) → C i<VAR>f : X ⟶ X'<VAR>Y : (j : J) → D j<VAR>s : I ⊕ J<GOAL>((CategoryTheory.Pi.sum C).map f).app Y s = match s with | Sum.inl i => f i | Sum.inr j => CategoryTheory.CategoryStruct.id (Y j)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f : X ≅ Y<VAR>i : I<GOAL>(CategoryTheory.Pi.isoApp f i).inv = f.inv i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f : X ≅ Y<VAR>i : I<GOAL>(CategoryTheory.Pi.isoApp f i).hom = f.hom i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X : (i : I) → C i<VAR>i : I<GOAL>CategoryTheory.Pi.isoApp (CategoryTheory.Iso.refl X) i = CategoryTheory.Iso.refl (X i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f : X ≅ Y<VAR>i : I<GOAL>CategoryTheory.Pi.isoApp f.symm i = (CategoryTheory.Pi.isoApp f i).symm
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y Z : (i : I) → C i<VAR>f : X ≅ Y<VAR>g : Y ≅ Z<VAR>i : I<GOAL>CategoryTheory.Pi.isoApp (f ≪≫ g) i = CategoryTheory.Pi.isoApp f i ≪≫ CategoryTheory.Pi.isoApp g i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>F : (i : I) → CategoryTheory.Functor (C i) (D i)<GOAL>∀ {X Y : (i : I) → C i} (α : X ⟶ Y) (i : I), (CategoryTheory.Functor.pi F).map α i = (F i).map (α i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>F : (i : I) → CategoryTheory.Functor (C i) (D i)<VAR>f : (i : I) → C i<VAR>i : I<GOAL>(CategoryTheory.Functor.pi F).obj f i = (F i).obj (f i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>f : (i : I) → CategoryTheory.Functor A (C i)<VAR>a : A<VAR>i : I<GOAL>(CategoryTheory.Functor.pi' f).obj a i = (f i).obj a
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>f : (i : I) → CategoryTheory.Functor A (C i)<GOAL>∀ {X Y : A} (h : X ⟶ Y) (i : I), (CategoryTheory.Functor.pi' f).map h i = (f i).map h
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>F : (i : I) → CategoryTheory.Functor A (C i)<VAR>i : I<VAR>X : A<GOAL>(CategoryTheory.Functor.pi'CompEval F i).hom.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>F : (i : I) → CategoryTheory.Functor A (C i)<VAR>i : I<VAR>X : A<GOAL>(CategoryTheory.Functor.pi'CompEval F i).inv.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>x x' : (i : I) → C i<VAR>h : x = x'<VAR>i : I<GOAL>CategoryTheory.eqToHom h i = CategoryTheory.eqToHom ⋯
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>f : (i : I) → CategoryTheory.Functor A (C i)<VAR>i : I<GOAL>(CategoryTheory.Functor.pi' f).comp (CategoryTheory.Pi.eval C i) = f i
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>f f' : CategoryTheory.Functor A ((i : I) → C i)<VAR>h : ∀ (i : I), f.comp (CategoryTheory.Pi.eval C i) = f'.comp (CategoryTheory.Pi.eval C i)<GOAL>f = f'
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>F G : (i : I) → CategoryTheory.Functor (C i) (D i)<VAR>α : (i : I) → F i ⟶ G i<VAR>f : (i : I) → C i<VAR>i : I<GOAL>(CategoryTheory.NatTrans.pi α).app f i = (α i).app (f i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F G : CategoryTheory.Functor E ((i : I) → C i)<VAR>τ : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ⟶ G.comp (CategoryTheory.Pi.eval C i)<VAR>X : E<VAR>i : I<GOAL>(CategoryTheory.NatTrans.pi' τ).app X i = (τ i).app X
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>F G : (i : I) → CategoryTheory.Functor (C i) (D i)<VAR>e : (i : I) → F i ≅ G i<GOAL>(CategoryTheory.NatIso.pi e).hom = CategoryTheory.NatTrans.pi fun i => (e i).hom
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>F G : (i : I) → CategoryTheory.Functor (C i) (D i)<VAR>e : (i : I) → F i ≅ G i<GOAL>(CategoryTheory.NatIso.pi e).inv = CategoryTheory.NatTrans.pi fun i => (e i).inv
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F G : CategoryTheory.Functor E ((i : I) → C i)<VAR>e : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ≅ G.comp (CategoryTheory.Pi.eval C i)<GOAL>(CategoryTheory.NatIso.pi' e).hom = CategoryTheory.NatTrans.pi' fun i => (e i).hom
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F G : CategoryTheory.Functor E ((i : I) → C i)<VAR>e : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ≅ G.comp (CategoryTheory.Pi.eval C i)<GOAL>(CategoryTheory.NatIso.pi' e).inv = CategoryTheory.NatTrans.pi' fun i => (e i).inv
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ ∀ (i : I), CategoryTheory.IsIso (f i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i j : I<VAR>h : i = j<GOAL>(CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).inv = CategoryTheory.eqToHom ⋯
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i j : I<VAR>h : i = j<GOAL>(CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).hom = CategoryTheory.eqToHom ⋯
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>f : J → I<VAR>i' j' : J<VAR>h : i' = j'<GOAL>(CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).inv = CategoryTheory.eqToHom ⋯
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>f : J → I<VAR>i' j' : J<VAR>h : i' = j'<GOAL>(CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).hom = CategoryTheory.eqToHom ⋯
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>e : J ≃ I<GOAL>(CategoryTheory.Pi.equivalenceOfEquiv C e).counitIso = CategoryTheory.NatIso.pi' fun i => ((CategoryTheory.Functor.pi' fun i' => CategoryTheory.Pi.eval C (e i')).associator (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i)) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.Functor.pi'CompEval (fun i' => CategoryTheory.Pi.eval C (e i')) (e.symm i)) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor ≪≫ CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C ⋯ ≪≫ (CategoryTheory.Pi.eval C i).leftUnitor.symm
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>e : J ≃ I<GOAL>(CategoryTheory.Pi.equivalenceOfEquiv C e).inverse = CategoryTheory.Functor.pi' fun i' => CategoryTheory.Pi.eval C (e i')
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>e : J ≃ I<GOAL>(CategoryTheory.Pi.equivalenceOfEquiv C e).functor = CategoryTheory.Functor.pi' fun i => (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i)).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).functor
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>e : J ≃ I<GOAL>(CategoryTheory.Pi.equivalenceOfEquiv C e).unitIso = CategoryTheory.NatIso.pi' fun i' => (CategoryTheory.Pi.eval (fun i => C (e i)) i').leftUnitor ≪≫ (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) ⋯).symm ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))) (CategoryTheory.Pi.eqToEquivalenceFunctorIso C ⇑e ⋯).symm ≪≫ (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp) (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ ((CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).associator (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval fun i => C (e i'))) (CategoryTheory.Pi.eval (fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor)).symm
<VAR>J : Type w₁<VAR>C' : Option J → Type u₁<VAR>(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)<GOAL>(CategoryTheory.Pi.optionEquivalence C').unitIso = CategoryTheory.NatIso.pi' fun i => match i with | none => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id ((i : Option J) → C' i)).comp (CategoryTheory.Pi.eval C' none)) | some i => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id ((i : Option J) → C' i)).comp (CategoryTheory.Pi.eval C' (some i)))
<VAR>J : Type w₁<VAR>C' : Option J → Type u₁<VAR>(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)<GOAL>(CategoryTheory.Pi.optionEquivalence C').functor = (CategoryTheory.Pi.eval C' none).prod' (CategoryTheory.Functor.pi' fun i => CategoryTheory.Pi.eval C' (some i))
<VAR>J : Type w₁<VAR>C' : Option J → Type u₁<VAR>(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)<GOAL>(CategoryTheory.Pi.optionEquivalence C').counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.pi' fun i => match i with | none => CategoryTheory.Prod.fst (C' none) ((j : J) → C' (some j)) | some i => (CategoryTheory.Prod.snd (C' none) ((j : J) → C' (some j))).comp (CategoryTheory.Pi.eval (fun j => C' (some j)) i)).comp ((CategoryTheory.Pi.eval C' none).prod' (CategoryTheory.Functor.pi' fun i => CategoryTheory.Pi.eval C' (some i))))
<VAR>J : Type w₁<VAR>C' : Option J → Type u₁<VAR>(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)<GOAL>(CategoryTheory.Pi.optionEquivalence C').inverse = CategoryTheory.Functor.pi' fun i => match i with | none => CategoryTheory.Prod.fst (C' none) ((j : J) → C' (some j)) | some i => (CategoryTheory.Prod.snd (C' none) ((j : J) → C' (some j))).comp (CategoryTheory.Pi.eval (fun j => C' (some j)) i)
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>E : (i : I) → C i ≌ D i<GOAL>(CategoryTheory.Equivalence.pi E).counitIso = CategoryTheory.NatIso.pi fun i => (E i).counitIso
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>E : (i : I) → C i ≌ D i<GOAL>(CategoryTheory.Equivalence.pi E).functor = CategoryTheory.Functor.pi fun i => (E i).functor
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>E : (i : I) → C i ≌ D i<GOAL>(CategoryTheory.Equivalence.pi E).unitIso = CategoryTheory.NatIso.pi fun i => (E i).unitIso
<VAR>I : Type w₀<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)<VAR>E : (i : I) → C i ≌ D i<GOAL>(CategoryTheory.Equivalence.pi E).inverse = CategoryTheory.Functor.pi fun i => (E i).inverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>x y : R<VAR>p : R[X]<GOAL>Polynomial.evalEval x y (Polynomial.C p) = Polynomial.eval x p
<VAR>R : Type u_1<VAR>Semiring R<VAR>x y : R<GOAL>Polynomial.evalEval x y Y = y
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>⇑(algebraMap R R[X][Y]) = Polynomial.CC
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x y : R<GOAL>∀ (a : R[X][Y]), (Polynomial.evalEvalRingHom x y) a = Polynomial.eval x (Polynomial.eval (Polynomial.C y) a)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x y : R<GOAL>⇑(Polynomial.evalEvalRingHom x y) = Polynomial.evalEval x y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<GOAL>Polynomial.evalEvalRingHom x = Polynomial.eval₂RingHom (Polynomial.evalRingHom x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<GOAL>Polynomial.eval₂ (Polynomial.evalRingHom x) = Polynomial.evalEval x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x y : R<VAR>p : R[X][Y]<GOAL>Polynomial.eval y (Polynomial.map (Polynomial.evalRingHom x) p) = Polynomial.evalEval x y p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X][Y]<VAR>q : R[X]<GOAL>Polynomial.eval (Polynomial.map f q) (Polynomial.map (Polynomial.mapRingHom f) p) = Polynomial.map f (Polynomial.eval q p)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X][Y]<VAR>q : R[X]<VAR>r : R<GOAL>Polynomial.eval (f r) (Polynomial.eval (Polynomial.map f q) (Polynomial.map (Polynomial.mapRingHom f) p)) = f (Polynomial.eval r (Polynomial.eval q p))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : R[X][Y]<VAR>x y : R<GOAL>Polynomial.evalEval (f x) (f y) (Polynomial.map (Polynomial.mapRingHom f) p) = f (Polynomial.evalEval x y p)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x y : S<GOAL>Polynomial.eval₂RingHom (Polynomial.eval₂RingHom f x) y = (Polynomial.evalEvalRingHom x y).comp (Polynomial.mapRingHom (Polynomial.mapRingHom f))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x y : S<VAR>p : R[X][Y]<GOAL>Polynomial.eval₂ (Polynomial.eval₂RingHom f x) y p = Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom f) p)
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>(Polynomial.evalRingHom (Polynomial.C Polynomial.X)).comp (Polynomial.eval₂RingHom (Polynomial.mapRingHom (algebraMap R R[X][Y])) (Polynomial.C Y)) = RingHom.id R[X][Y]
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : R[X][Y]<GOAL>Polynomial.eval (Polynomial.C Polynomial.X) (Polynomial.eval₂ (Polynomial.mapRingHom (algebraMap R R[X][Y])) (Polynomial.C Y) p) = p
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>p : R[X][Y]<VAR>h : Polynomial.evalEval x y p = 0<GOAL>∀ (a : R[X][Y] ⧸ Submodule.toAddSubgroup (Ideal.span {p})), (AdjoinRoot.evalEval h) a = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {p})) ↑(Polynomial.eval₂RingHom (Polynomial.evalRingHom x) y) ⋯) a
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>p : R[X][Y]<VAR>h : Polynomial.evalEval x y p = 0<VAR>g : R[X][Y]<GOAL>(AdjoinRoot.evalEval h) ((AdjoinRoot.mk p) g) = Polynomial.evalEval x y g
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R A[X]) r = Polynomial.C ((algebraMap R A) r)
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>((algebraMap R A[X]) r).toFinsupp = (algebraMap R (AddMonoidAlgebra A ℕ)) r
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>{ toFinsupp := (algebraMap R (AddMonoidAlgebra A ℕ)) r } = (algebraMap R A[X]) r
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>Polynomial.C r = (algebraMap R R[X]) r
<VAR>R : Type u<VAR>CommSemiring R<GOAL>algebraMap R R[X] = Polynomial.C
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>∀ (a : A), Polynomial.CAlgHom a = Polynomial.C a
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f g : A[X] →ₐ[R] B<VAR>hC : f.comp Polynomial.CAlgHom = g.comp Polynomial.CAlgHom<VAR>hX : f Polynomial.X = g Polynomial.X<GOAL>f = g
<VAR>R : Type u<VAR>CommSemiring R<VAR>toFinsupp : AddMonoidAlgebra R ℕ<GOAL>((Polynomial.toFinsuppIsoAlg R).symm toFinsupp).toFinsupp = toFinsupp
<VAR>R : Type u<VAR>CommSemiring R<VAR>self : R[X]<GOAL>(Polynomial.toFinsuppIsoAlg R) self = self.toFinsupp
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>p : R[X]<VAR>f : A →ₐ[R] B<VAR>a : A<GOAL>f (Polynomial.eval₂ (algebraMap R A) a p) = Polynomial.eval₂ (algebraMap R B) (f a) p
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : R[X]<VAR>f : R[X] →ₐ[R] A<GOAL>Polynomial.eval₂ (algebraMap R A) (f Polynomial.X) p = f p
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>Ring R<VAR>Ring S<VAR>p : ℤ[X]<VAR>f : R →+* S<VAR>r : R<GOAL>f (Polynomial.eval₂ (Int.castRingHom R) r p) = Polynomial.eval₂ (Int.castRingHom S) (f r) p
<VAR>R : Type u_3<VAR>Ring R<VAR>p : ℤ[X]<VAR>f : ℤ[X] →+* R<GOAL>Polynomial.eval₂ (Int.castRingHom R) (f Polynomial.X) p = f p
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>b : B<VAR>hf : ∀ (a : A), Commute (f a) b<VAR>p : A[X]<GOAL>(Polynomial.eval₂AlgHom' f b hf) p = Polynomial.eval₂ (↑f) b p
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>⇑(Polynomial.mapAlgHom f) = Polynomial.map ↑f
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Polynomial.mapAlgHom (AlgHom.id R A) = AlgHom.id R A[X]
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>↑(Polynomial.mapAlgHom f) = Polynomial.mapRingHom ↑f
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type z<VAR>Semiring C<VAR>Algebra R C<VAR>f : B →ₐ[R] C<VAR>g : A →ₐ[R] B<GOAL>(Polynomial.mapAlgHom f).comp (Polynomial.mapAlgHom g) = Polynomial.mapAlgHom (f.comp g)
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>Polynomial.mapAlgHom f = Polynomial.eval₂AlgHom' (Polynomial.CAlgHom.comp f) Polynomial.X ⋯
<VAR>R : Type u<VAR>A : Type z<VAR>B : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<GOAL>⇑(Polynomial.mapAlgEquiv f) = Polynomial.map ↑f
<VAR>R : Type u<VAR>A : Type z<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Polynomial.mapAlgEquiv AlgEquiv.refl = AlgEquiv.refl