awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.right })

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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
refine : obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone ≅ (b.ofIso eP eQ).toCone
⊢ IsLimit (b.ofIso eP eQ).toCone

Tactic:
refine (IsLimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isLimit

Premises used: Equiv.toFun, CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit, CategoryTheory.Limits.mapPairIso, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ BinaryFan.fst (obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone) =
    Iso.hom (Iso.refl (Cone.pt (F := pair P' Q') (obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone))) ≫
      BinaryFan.fst (b.ofIso eP eQ).toCone

Tactic:
simp [BinaryFan.fst]

Premises used: CategoryTheory.Limits.BinaryFan.fst
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ BinaryFan.snd (obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone) =
    Iso.hom (Iso.refl (Cone.pt (F := pair P' Q') (obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone))) ≫
      BinaryFan.snd (b.ofIso eP eQ).toCone

Tactic:
simp [BinaryFan.snd]

Premises used: CategoryTheory.Limits.BinaryFan.snd
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone ≅ (b.ofIso eP eQ).toCone

Tactic:
exact BinaryFan.ext (Iso.refl _) (by simp [BinaryFan.fst])
      (by simp [BinaryFan.snd])

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.BinaryFan.ext
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
refine : obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone ≅ (b.ofIso eP eQ).toCocone
⊢ IsColimit (b.ofIso eP eQ).toCocone

Tactic:
refine (IsColimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isColimit

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, Equiv.toFun, CategoryTheory.Limits.mapPairIso, CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ CategoryStruct.comp (Y :=
      obj.{0, uC', 0, uC}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt (F := pair P' Q') (obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone)))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone))
      (Iso.hom
        (Iso.refl (Cocone.pt (F := pair P' Q') (obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone)))) =
    BinaryCofan.inl (b.ofIso eP eQ).toCocone

Tactic:
simp [BinaryCofan.inl]

Premises used: CategoryTheory.Limits.BinaryCofan.inl
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ CategoryStruct.comp (Y :=
      obj.{0, uC', 0, uC}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt (F := pair P' Q') (obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone)))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone))
      (Iso.hom
        (Iso.refl (Cocone.pt (F := pair P' Q') (obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone)))) =
    BinaryCofan.inr (b.ofIso eP eQ).toCocone

Tactic:
simp [BinaryCofan.inr]

Premises used: CategoryTheory.Limits.BinaryCofan.inr
-- 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 P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone ≅ (b.ofIso eP eQ).toCocone

Tactic:
exact BinaryCofan.ext (Iso.refl _) (by simp [BinaryCofan.inl])
      (by simp [BinaryCofan.inr])

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.BinaryCofan.ext
-- 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
X Y : C
b : BinaryBicone.{uC', uC} X Y
x : b.toBicone.IsBilimit
h : IsLimit b.toBicone.toCone
h' : IsColimit b.toBicone.toCocone
dsimp :
  {
      isLimit :=
        (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone)
          ((b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h),
      isColimit :=
        (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone)
          ((b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.toBicone.IsBilimit }
⊢ (fun (h : b.IsBilimit) ↦
        ({ isLimit := (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h.isLimit,
            isColimit :=
              (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h.isColimit } :
          b.toBicone.IsBilimit))
      ((fun (h : b.toBicone.IsBilimit) ↦
          ({ isLimit := (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h.isLimit,
              isColimit :=
                (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h.isColimit } :
            b.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.toBicone.IsBilimit }

Tactic:
dsimp only
-- 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
X Y : C
b : BinaryBicone.{uC', uC} X Y
x : b.toBicone.IsBilimit
h : IsLimit b.toBicone.toCone
h' : IsColimit b.toBicone.toCocone
⊢ {
      isLimit :=
        (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone)
          ((b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h),
      isColimit :=
        (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone)
          ((b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.toBicone.IsBilimit }

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
X Y : C
b : BinaryBicone.{uC', uC} X Y
x : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
dsimp :
  {
      isLimit :=
        (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone)
          ((b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h),
      isColimit :=
        (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone)
          ((b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.IsBilimit }
⊢ (fun (h : b.toBicone.IsBilimit) ↦
        ({ isLimit := (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h.isLimit,
            isColimit :=
              (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h.isColimit } :
          b.IsBilimit))
      ((fun (h : b.IsBilimit) ↦
          ({ isLimit := (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h.isLimit,
              isColimit :=
                (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h.isColimit } :
            b.toBicone.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.IsBilimit }

Tactic:
dsimp only
-- 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
X Y : C
b : BinaryBicone.{uC', uC} X Y
x : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ {
      isLimit :=
        (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone)
          ((b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h),
      isColimit :=
        (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone)
          ((b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.IsBilimit }

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
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
x : b.toBinaryBicone.IsBilimit
h : IsLimit b.toBinaryBicone.toCone
h' : IsColimit b.toBinaryBicone.toCocone
dsimp :
  {
      isLimit :=
        (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone)
          ((b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h),
      isColimit :=
        (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
          ((b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.toBinaryBicone.IsBilimit }
⊢ (fun (h : b.IsBilimit) ↦
        ({
            isLimit :=
              (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h.isLimit,
            isColimit :=
              (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
                h.isColimit } :
          b.toBinaryBicone.IsBilimit))
      ((fun (h : b.toBinaryBicone.IsBilimit) ↦
          ({ isLimit := (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h.isLimit,
              isColimit :=
                (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
                  h.isColimit } :
            b.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.toBinaryBicone.IsBilimit }

Tactic:
dsimp only
-- 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
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
x : b.toBinaryBicone.IsBilimit
h : IsLimit b.toBinaryBicone.toCone
h' : IsColimit b.toBinaryBicone.toCocone
⊢ {
      isLimit :=
        (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone)
          ((b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h),
      isColimit :=
        (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
          ((b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.toBinaryBicone.IsBilimit }

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
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
x : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
dsimp :
  {
      isLimit :=
        (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone)
          ((b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h),
      isColimit :=
        (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
          ((b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.IsBilimit }
⊢ (fun (h : b.toBinaryBicone.IsBilimit) ↦
        ({ isLimit := (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h.isLimit,
            isColimit :=
              (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
                h.isColimit } :
          b.IsBilimit))
      ((fun (h : b.IsBilimit) ↦
          ({
              isLimit :=
                (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h.isLimit,
              isColimit :=
                (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
                  h.isColimit } :
            b.toBinaryBicone.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.IsBilimit }

Tactic:
dsimp only
-- 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
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
x : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ {
      isLimit :=
        (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone)
          ((b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h),
      isColimit :=
        (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
          ((b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone) h') } =
    { isLimit := h, isColimit := h' : b.IsBilimit }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
d : BinaryBiproductData.{uC', uC} P Q
⊢ HasBinaryBiproduct.{uC', uC} P Q

Tactic:
⟨Nonempty.intro d⟩

Premises used: CategoryTheory.Limits.HasBinaryBiproduct.mk', Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
inst_2 : HasFiniteBiproducts.{uC', uC} C
⊢ HasBinaryBiproducts.{uC', uC} C

Tactic:
{ has_binary_biproduct := fun P Q =>
      HasBinaryBiproduct.mk
        { bicone := (biproduct.bicone (pairFunction P Q)).toBinaryBicone
          isBilimit := (Bicone.toBinaryBiconeIsBilimit _).symm (biproduct.isBilimit _) } }

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.toBinaryBicone, CategoryTheory.Limits.biproduct.isBilimit, CategoryTheory.Limits.pairFunction, CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit, Equiv.symm, CategoryTheory.Limits.HasBinaryBiproducts.mk, DFunLike.coe, CategoryTheory.Limits.HasBinaryBiproduct.mk, CategoryTheory.Limits.BinaryBiproductData.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 : C
inst_4 : HasBinaryBiproduct.{uC', uC} P Q
⊢ HasLimit.{0, 0, uC', uC} (pair P Q)

Tactic:
HasLimit.mk ⟨_, BinaryBiproduct.isLimit P Q⟩

Premises used: CategoryTheory.Limits.BinaryBiproduct.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.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 : C
inst_4 : HasBinaryBiproduct.{uC', uC} P Q
⊢ HasColimit.{0, 0, uC', uC} (pair P Q)

Tactic:
HasColimit.mk ⟨_, BinaryBiproduct.isColimit P Q⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.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
⊢ Eq.{uC' + 1} (α := BinaryBicone.pt.{uC', uC} (bicone X Y) ⟶ X) (BinaryBicone.fst (bicone X Y)) biprod.fst

Tactic:
rfl

Premises used: 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
⊢ Eq.{uC' + 1} (α := BinaryBicone.pt.{uC', uC} (bicone X Y) ⟶ Y) (BinaryBicone.snd (bicone X Y)) biprod.snd

Tactic:
rfl

Premises used: 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
⊢ Eq.{uC' + 1} (α := X ⟶ BinaryBicone.pt.{uC', uC} (bicone X Y)) (BinaryBicone.inl (bicone X Y)) biprod.inl

Tactic:
rfl

Premises used: 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
⊢ Eq.{uC' + 1} (α := Y ⟶ BinaryBicone.pt.{uC', uC} (bicone X Y)) (BinaryBicone.inr (bicone X Y)) biprod.inr

Tactic:
rfl

Premises used: 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
⊢ Eq.{uC' + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl fst) (𝟙 X)

Tactic:
(BinaryBiproduct.bicone X Y).inl_fst

Premises used: CategoryTheory.Limits.BinaryBicone.inl_fst, CategoryTheory.Limits.BinaryBiproduct.bicone
-- 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
⊢ Eq.{uC' + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl snd) 0

Tactic:
(BinaryBiproduct.bicone X Y).inl_snd

Premises used: CategoryTheory.Limits.BinaryBiproduct.bicone, CategoryTheory.Limits.BinaryBicone.inl_snd
-- 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
⊢ Eq.{uC' + 1} (α := Y ⟶ X) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr fst) 0

Tactic:
(BinaryBiproduct.bicone X Y).inr_fst

Premises used: CategoryTheory.Limits.BinaryBiproduct.bicone, CategoryTheory.Limits.BinaryBicone.inr_fst
-- 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
⊢ Eq.{uC' + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr snd) (𝟙 Y)

Tactic:
(BinaryBiproduct.bicone X Y).inr_snd

Premises used: CategoryTheory.Limits.BinaryBicone.inr_snd, CategoryTheory.Limits.BinaryBiproduct.bicone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
f : W ⟶ X
g : W ⟶ Y
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift f g) fst = f

Tactic:
(BinaryBiproduct.isLimit X Y).fac _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isLimit, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
f : W ⟶ X
g : W ⟶ Y
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift f g) snd = g

Tactic:
(BinaryBiproduct.isLimit X Y).fac _ ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isLimit, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
f : X ⟶ W
g : Y ⟶ W
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc f g) = f

Tactic:
(BinaryBiproduct.isColimit X Y).fac _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, 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 : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
f : X ⟶ W
g : Y ⟶ W
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc f g) = g

Tactic:
(BinaryBiproduct.isColimit X Y).fac _ ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryBiproduct.isColimit