awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
h₁ :
  Eq.{uC' + 1} (α := X ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X)))
            { as := WalkingPair.left : Discrete WalkingPair } ≫
          NatTrans.app (mapPair f g) { as := WalkingPair.left }) :
      X ⟶ Y)
    (g ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair } ⟶
              obj.{0, uC', 0, uC}
                (obj (const (Discrete WalkingPair))
                  (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))))
                { as := WalkingPair.right : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left }) :
      X ⟶ Y)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map f g)) fst =
    CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map' f g)) fst

Tactic:
simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right, CategoryTheory.Limits.BinaryBicone.toCone_π_app_left, CategoryTheory.Limits.mapPair_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq.{uC' + 1} (α := X ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X)))
            { as := WalkingPair.left : Discrete WalkingPair } ≫
          NatTrans.app (mapPair f g) { as := WalkingPair.left }) :
      X ⟶ Y)
    (g ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair } ⟶
              obj.{0, uC', 0, uC}
                (obj (const (Discrete WalkingPair))
                  (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))))
                { as := WalkingPair.right : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left }) :
      X ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
h₁ :
  Eq.{uC' + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right } :
          obj.{0, uC', 0, uC} (pair W X) { as := WalkingPair.right : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))))
              { as := WalkingPair.right : Discrete WalkingPair })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right } ≫ g :
          obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone W X))))
              { as := WalkingPair.right : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair }) :
      X ⟶ Z)
    (g ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair } ⟶
              obj.{0, uC', 0, uC}
                (obj (const (Discrete WalkingPair))
                  (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))))
                { as := WalkingPair.right : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right }) :
      X ⟶ Z)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map f g)) snd =
    CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map' f g)) snd

Tactic:
simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.toCone_π_app_right, CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right, CategoryTheory.Limits.mapPair_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq.{uC' + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right } :
          obj.{0, uC', 0, uC} (pair W X) { as := WalkingPair.right : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))))
              { as := WalkingPair.right : Discrete WalkingPair })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right } ≫ g :
          obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone W X))))
              { as := WalkingPair.right : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair }) :
      X ⟶ Z)
    (g ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair } ⟶
              obj.{0, uC', 0, uC}
                (obj (const (Discrete WalkingPair))
                  (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))))
                { as := WalkingPair.right : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right }) :
      X ⟶ Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
⊢ IsSplitMono.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl

Tactic:
IsSplitMono.mk' { retraction := biprod.fst }

Premises used: CategoryTheory.SplitMono.mk, CategoryTheory.Limits.biprod.fst, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
⊢ IsSplitMono.{uC', uC} (C := C) (X := Y) (Y := biprod.{uC', uC} X Y) inr

Tactic:
IsSplitMono.mk' { retraction := biprod.snd }

Premises used: CategoryTheory.SplitMono.mk, CategoryTheory.Limits.biprod.snd, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
⊢ IsSplitEpi.{uC', uC} (C := C) (X := biprod.{uC', uC} X Y) fst

Tactic:
IsSplitEpi.mk' { section_ := biprod.inl }

Premises used: CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.biprod.inl, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
⊢ IsSplitEpi.{uC', uC} (C := C) (X := biprod.{uC', uC} X Y) snd

Tactic:
IsSplitEpi.mk' { section_ := biprod.inr }

Premises used: CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.biprod.inr, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := biprod.{uC', uC} W X ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (map f g) fst) (fst ≫ f)

Tactic:
IsLimit.map_π _ _ _ (⟨WalkingPair.left⟩ : Discrete WalkingPair)

Premises used: CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := biprod.{uC', uC} W X ⟶ Z) (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (map f g) snd) (snd ≫ g)

Tactic:
IsLimit.map_π _ _ _ (⟨WalkingPair.right⟩ : Discrete WalkingPair)

Premises used: CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
rw : Eq (α := W ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) (f ≫ inl)
⊢ Eq (α := W ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map f g)) (f ≫ inl)

Tactic:
rw [biprod.map_eq_map']

Premises used: CategoryTheory.Limits.biprod.map_eq_map'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := W ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) (f ≫ inl)

Tactic:
IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isColimit, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := W ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) (f ≫ inl)

Tactic:
exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isColimit, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
rw : Eq (α := X ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map' f g)) (g ≫ inr)
⊢ Eq (α := X ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map f g)) (g ≫ inr)

Tactic:
rw [biprod.map_eq_map']

Premises used: CategoryTheory.Limits.biprod.map_eq_map'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := X ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map' f g)) (g ≫ inr)

Tactic:
IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := X ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map' f g)) (g ≫ inr)

Tactic:
exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := b.toCone.pt ⟶ Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)))
    (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (lift b.fst b.snd)

Tactic:
rfl

Premises used: CategoryTheory.Limits.BinaryBicone.toCone, CategoryTheory.Limits.BinaryFan.IsLimit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr)

Tactic:
biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.biprod.hom_ext', CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
refine_1 :
  ∀ (j : Discrete WalkingPair),
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
          (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
        b.toCone.π.app j =
      CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr) ≫ b.toCone.π.app j
refine_2 :
  ∀ (j : Discrete WalkingPair),
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
          (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
        b.toCone.π.app j =
      CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr) ≫ b.toCone.π.app j
⊢ Eq (α := Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr)

Tactic:
refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.biprod.hom_ext', CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
refine_1 :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app j)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
        (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
      b.toCone.π.app j =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr) ≫ b.toCone.π.app j

Tactic:
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
refine_1 :
  Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))
refine_1₁ :
  Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.right }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }))
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app j)

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
refine_2 :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app j)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
        (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
      b.toCone.π.app j =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr) ≫ b.toCone.π.app j

Tactic:
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
refine_2 :
  Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))
refine_2₁ :
  Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.right }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }))
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app j)

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.right }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))

Tactic:
simp