ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Z ⟶ W<GOAL>CategoryTheory.Limits.prod.map f g ≫ (CategoryTheory.Limits.prod.braiding Y W).hom = (CategoryTheory.Limits.prod.braiding X Z).hom ≫ CategoryTheory.Limits.prod.map g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.Limits.HasBinaryProduct P Q<VAR>CategoryTheory.Limits.HasBinaryProduct Q P<GOAL>CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst ≫ CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst = 𝟙 (P ⨯ Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.Limits.HasBinaryProduct P Q<VAR>CategoryTheory.Limits.HasBinaryProduct Q P<GOAL>(CategoryTheory.Limits.prod.braiding P Q).hom ≫ (CategoryTheory.Limits.prod.braiding Q P).hom = 𝟙 (P ⨯ Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>P Q R : C<GOAL>(CategoryTheory.Limits.prod.associator P Q R).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.fst ≫ CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.fst ≫ CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>P Q R : C<GOAL>(CategoryTheory.Limits.prod.associator P Q R).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.Limits.prod.snd ≫ CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.snd ≫ CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>W X Y Z : C<GOAL>CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom (𝟙 Z) ≫ (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom ≫ CategoryTheory.Limits.prod.map (𝟙 W) (CategoryTheory.Limits.prod.associator X Y Z).hom = (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom ≫ (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃ ≫ (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom = (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom ≫ CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>P : C<VAR>CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P<GOAL>(CategoryTheory.Limits.prod.leftUnitor P).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from P) (𝟙 P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>P : C<VAR>CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P<GOAL>(CategoryTheory.Limits.prod.leftUnitor P).hom = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>P : C<VAR>CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)<GOAL>(CategoryTheory.Limits.prod.rightUnitor P).hom = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>P : C<VAR>CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)<GOAL>(CategoryTheory.Limits.prod.rightUnitor P).inv = CategoryTheory.Limits.prod.lift (𝟙 P) (CategoryTheory.Limits.terminal.from P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.prod.map (𝟙 (⊤_ C)) f ≫ (CategoryTheory.Limits.prod.leftUnitor Y).hom = (CategoryTheory.Limits.prod.leftUnitor X).hom ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.prod.leftUnitor X).inv ≫ CategoryTheory.Limits.prod.map (𝟙 (⊤_ C)) f = f ≫ (CategoryTheory.Limits.prod.leftUnitor Y).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.prod.map f (𝟙 (⊤_ C)) ≫ (CategoryTheory.Limits.prod.rightUnitor Y).hom = (CategoryTheory.Limits.prod.rightUnitor X).hom ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.prod.rightUnitor X).inv ≫ CategoryTheory.Limits.prod.map f (𝟙 (⊤_ C)) = f ≫ (CategoryTheory.Limits.prod.rightUnitor Y).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.prod.associator X (⊤_ C) Y).hom ≫ CategoryTheory.Limits.prod.map (𝟙 X) (CategoryTheory.Limits.prod.leftUnitor Y).hom = CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.rightUnitor X).hom (𝟙 Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.coprod.braiding P Q).hom = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.coprod.braiding P Q).inv = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q : C<GOAL>CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl = 𝟙 (P ⨿ Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.coprod.braiding P Q).hom ≫ (CategoryTheory.Limits.coprod.braiding Q P).hom = 𝟙 (P ⨿ Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q R : C<GOAL>(CategoryTheory.Limits.coprod.associator P Q R).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.Limits.coprod.inr)) (CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.Limits.coprod.inr)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q R : C<GOAL>(CategoryTheory.Limits.coprod.associator P Q R).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>W X Y Z : C<GOAL>CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.associator W X Y).hom (𝟙 Z) ≫ (CategoryTheory.Limits.coprod.associator W (X ⨿ Y) Z).hom ≫ CategoryTheory.Limits.coprod.map (𝟙 W) (CategoryTheory.Limits.coprod.associator X Y Z).hom = (CategoryTheory.Limits.coprod.associator (W ⨿ X) Y Z).hom ≫ (CategoryTheory.Limits.coprod.associator W X (Y ⨿ Z)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.map f₁ f₂) f₃ ≫ (CategoryTheory.Limits.coprod.associator Y₁ Y₂ Y₃).hom = (CategoryTheory.Limits.coprod.associator X₁ X₂ X₃).hom ≫ CategoryTheory.Limits.coprod.map f₁ (CategoryTheory.Limits.coprod.map f₂ f₃)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>P : C<GOAL>(CategoryTheory.Limits.coprod.leftUnitor P).inv = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>P : C<GOAL>(CategoryTheory.Limits.coprod.leftUnitor P).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to P) (𝟙 P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>P : C<GOAL>(CategoryTheory.Limits.coprod.rightUnitor P).hom = CategoryTheory.Limits.coprod.desc (𝟙 P) (CategoryTheory.Limits.initial.to P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>P : C<GOAL>(CategoryTheory.Limits.coprod.rightUnitor P).inv = CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.coprod.associator X (⊥_ C) Y).hom ≫ CategoryTheory.Limits.coprod.map (𝟙 X) (CategoryTheory.Limits.coprod.leftUnitor Y).hom = CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.rightUnitor X).hom (𝟙 Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (T : C), (CategoryTheory.Limits.prod.functor.map f).app T = CategoryTheory.Limits.prod.map f (𝟙 T)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.prod.functor.obj X).obj Y = (X ⨯ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.prod.functor.obj X).map g = CategoryTheory.Limits.prod.map (𝟙 X) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X : C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.coprod.functor.obj X).map g = CategoryTheory.Limits.coprod.map (𝟙 X) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.coprod.functor.obj X).obj Y = (X ⨿ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (T : C), (CategoryTheory.Limits.coprod.functor.map f).app T = CategoryTheory.Limits.coprod.map f (𝟙 T)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<GOAL>CategoryTheory.Limits.prodComparison F A B ≫ CategoryTheory.Limits.prod.fst = F.map CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<GOAL>CategoryTheory.Limits.prodComparison F A B ≫ CategoryTheory.Limits.prod.snd = F.map CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct A' B'<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<GOAL>F.map (CategoryTheory.Limits.prod.map f g) ≫ CategoryTheory.Limits.prodComparison F A' B' = CategoryTheory.Limits.prodComparison F A B ≫ CategoryTheory.Limits.prod.map (F.map f) (F.map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasBinaryProducts D<VAR>F : C ⥤ D<VAR>A B : C<GOAL>(CategoryTheory.Limits.prodComparisonNatTrans F A).app B = CategoryTheory.Limits.prodComparison F A B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)<GOAL>CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B) ≫ F.map CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)<GOAL>CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B) ≫ F.map CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct A' B'<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')<GOAL>CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B) ≫ F.map (CategoryTheory.Limits.prod.map f g) = CategoryTheory.Limits.prod.map (F.map f) (F.map g) ≫ CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasBinaryProducts D<VAR>A : C<VAR>∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)<GOAL>(CategoryTheory.Limits.prodComparisonNatIso F A).hom = CategoryTheory.Limits.prodComparisonNatTrans F A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasBinaryProducts D<VAR>A : C<VAR>∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)<GOAL>(CategoryTheory.Limits.prodComparisonNatIso F A).inv = (CategoryTheory.asIso { app := fun B => CategoryTheory.Limits.prodComparison F A B, naturality := ⋯ }).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryProduct A B<VAR>CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)<VAR>CategoryTheory.Limits.HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))<VAR>CategoryTheory.Limits.HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)<GOAL>CategoryTheory.Limits.prodComparison (F ⋙ G) A B = G.map (CategoryTheory.Limits.prodComparison F A B) ≫ CategoryTheory.Limits.prodComparison G (F.obj A) (F.obj B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A B<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)<GOAL>CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.Limits.coprodComparison F A B = F.map CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A B<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)<GOAL>CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.Limits.coprodComparison F A B = F.map CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A B<VAR>CategoryTheory.Limits.HasBinaryCoproduct A' B'<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<GOAL>CategoryTheory.Limits.coprodComparison F A B ≫ F.map (CategoryTheory.Limits.coprod.map f g) = CategoryTheory.Limits.coprod.map (F.map f) (F.map g) ≫ CategoryTheory.Limits.coprodComparison F A' B'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasBinaryCoproducts D<VAR>F : C ⥤ D<VAR>A B : C<GOAL>(CategoryTheory.Limits.coprodComparisonNatTrans F A).app B = CategoryTheory.Limits.coprodComparison F A B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A B<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)<GOAL>F.map CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B) = CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A B<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)<GOAL>F.map CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B) = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A B<VAR>CategoryTheory.Limits.HasBinaryCoproduct A' B'<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')<GOAL>CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B) ≫ CategoryTheory.Limits.coprod.map (F.map f) (F.map g) = F.map (CategoryTheory.Limits.coprod.map f g) ≫ CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasBinaryCoproducts D<VAR>A : C<VAR>∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)<GOAL>(CategoryTheory.Limits.coprodComparisonNatIso F A).inv = (CategoryTheory.asIso { app := fun B => CategoryTheory.Limits.coprodComparison F A B, naturality := ⋯ }).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasBinaryCoproducts D<VAR>A : C<VAR>∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)<GOAL>(CategoryTheory.Limits.coprodComparisonNatIso F A).hom = CategoryTheory.Limits.coprodComparisonNatTrans F A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A : C<GOAL>∀ (a : CategoryTheory.Over A) {X Y : CategoryTheory.Over A} (k : X ⟶ Y), a.coprodObj.map k = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map (𝟙 ((𝟭 C).obj a.left)) k.left) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A : C<GOAL>∀ (a g : CategoryTheory.Over A), a.coprodObj.obj g = CategoryTheory.Over.mk (CategoryTheory.Limits.coprod.desc a.hom g.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A : C<GOAL>∀ {X Y : CategoryTheory.Over A} (k : X ⟶ Y) (g : CategoryTheory.Over A), (CategoryTheory.Over.coprod.map k).app g = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A : C<VAR>f : CategoryTheory.Over A<GOAL>CategoryTheory.Over.coprod.obj f = f.coprodObj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>self : CategoryTheory.Limits.IndObjectPresentation A<GOAL>CategoryTheory.IsFiltered self.I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type v<VAR>CategoryTheory.SmallCategory I<VAR>CategoryTheory.IsFiltered I<VAR>F : CategoryTheory.Functor I C<VAR>c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).I = I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type v<VAR>CategoryTheory.SmallCategory I<VAR>CategoryTheory.IsFiltered I<VAR>F : CategoryTheory.Functor I C<VAR>c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).ℐ = inst✝
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type v<VAR>CategoryTheory.SmallCategory I<VAR>CategoryTheory.IsFiltered I<VAR>F : CategoryTheory.Functor I C<VAR>c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).ι = c.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type v<VAR>CategoryTheory.SmallCategory I<VAR>CategoryTheory.IsFiltered I<VAR>F : CategoryTheory.Functor I C<VAR>c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).F = F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type v<VAR>CategoryTheory.SmallCategory I<VAR>CategoryTheory.IsFiltered I<VAR>F : CategoryTheory.Functor I C<VAR>c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).isColimit = hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<GOAL>P.cocone.pt = A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<GOAL>(P.extend η).F = P.F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<VAR>X : P.I<GOAL>∀ (X_1 : Cᵒᵖ) (a : ((Opposite.unop (Opposite.op (P.F.comp CategoryTheory.yoneda))).obj X).obj X_1), ((P.extend η).ι.app X).app X_1 a = η.app X_1 ((P.cocone.ι.app X).app X_1 a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<GOAL>(P.extend η).ℐ = P.ℐ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<GOAL>(P.extend η).I = P.I