awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
left :
  Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    (b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
    (s.ι.app { as := WalkingPair.left })
right :
  Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    (b.toCocone.ι.app { as := WalkingPair.right } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
    (s.ι.app { as := WalkingPair.right })
⊢ b.toCocone.ι.app j ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) = s.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    (b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
    (s.ι.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    (b.toCocone.ι.app { as := WalkingPair.right } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
    (s.ι.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    (b.toCocone.ι.app { as := WalkingPair.left } ≫ m) (s.ι.app { as := WalkingPair.left })

Tactic:
have hₗ := h ⟨.left⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.inl ≫ m = s.ι.app { as := WalkingPair.left }
hᵣ : b.inr ≫ m = s.ι.app { as := WalkingPair.right }
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s

Tactic:
simpa [← hₗ, ← hᵣ] using total.symm =≫ m

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
i : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
    (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left })
right :
  Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right })
    (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.right })
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
i : b.IsBilimit
⊢ Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
    (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
i : b.IsBilimit
⊢ Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right })
    (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
⊢ HasBinaryBiproduct.{v, u} X Y

Tactic:
HasBinaryBiproduct.mk
    { bicone := b
      isBilimit := isBinaryBilimitOfTotal b total }

Premises used: CategoryTheory.Limits.isBinaryBilimitOfTotal, CategoryTheory.Limits.HasBinaryBiproduct.mk, CategoryTheory.Limits.BinaryBiproductData.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
x : ∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = NatTrans.app (Cone.π (BinaryFan.mk (𝟙 X) 0)) j
⊢ t.inl = BinaryFan.IsLimit.lift ht (𝟙 X) 0

Tactic:
apply ht.uniq (BinaryFan.mk (𝟙 X) 0)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.IsLimit.uniq, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ Eq (α :=
    Cone.pt.{0, v, 0, u} (F := pair X Y) (BinaryFan.mk (𝟙 X) 0) ⟶
      obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (t.inl ≫ t.toCone.π.app { as := WalkingPair.left })
    (NatTrans.app (Cone.π (BinaryFan.mk (𝟙 X) 0)) { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ Eq (α :=
    Cone.pt.{0, v, 0, u} (F := pair X Y) (BinaryFan.mk (𝟙 X) 0) ⟶
      obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (t.inl ≫ t.toCone.π.app { as := WalkingPair.right })
    (NatTrans.app (Cone.π (BinaryFan.mk (𝟙 X) 0)) { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
x : ∀ (j : Discrete WalkingPair), t.inr ≫ t.toCone.π.app j = NatTrans.app (Cone.π (BinaryFan.mk 0 (𝟙 Y))) j
⊢ t.inr = BinaryFan.IsLimit.lift ht 0 (𝟙 Y)

Tactic:
apply ht.uniq (BinaryFan.mk 0 (𝟙 Y))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.IsLimit.uniq, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ Eq (α :=
    Cone.pt.{0, v, 0, u} (F := pair X Y) (BinaryFan.mk 0 (𝟙 Y)) ⟶
      obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (t.inr ≫ t.toCone.π.app { as := WalkingPair.left })
    (NatTrans.app (Cone.π (BinaryFan.mk 0 (𝟙 Y))) { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ Eq (α :=
    Cone.pt.{0, v, 0, u} (F := pair X Y) (BinaryFan.mk 0 (𝟙 Y)) ⟶
      obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (t.inr ≫ t.toCone.π.app { as := WalkingPair.right })
    (NatTrans.app (Cone.π (BinaryFan.mk 0 (𝟙 Y))) { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
BinaryFan.IsLimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
refine_1 : (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.fst t.toCone = 𝟙 t.pt ≫ BinaryFan.fst t.toCone
refine_2 : (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.snd t.toCone = 𝟙 t.pt ≫ BinaryFan.snd t.toCone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
refine BinaryFan.IsLimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.fst t.toCone = 𝟙 t.pt ≫ BinaryFan.fst t.toCone

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.snd t.toCone = 𝟙 t.pt ≫ BinaryFan.snd t.toCone

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cone.{0, v, 0, u} (pair X Y)
ht : IsLimit t
⊢ HAdd.hAdd (α := BinaryBicone.pt (BinaryBicone.ofLimitCone ht) ⟶ BinaryBicone.pt (BinaryBicone.ofLimitCone ht))
        (BinaryBicone.fst (BinaryBicone.ofLimitCone ht) ≫ BinaryBicone.inl (BinaryBicone.ofLimitCone ht))
        (BinaryBicone.snd (BinaryBicone.ofLimitCone ht) ≫ BinaryBicone.inr (BinaryBicone.ofLimitCone ht)) ≫
      BinaryFan.fst t =
    𝟙 (BinaryBicone.pt (BinaryBicone.ofLimitCone ht)) ≫ BinaryFan.fst t

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cone.{0, v, 0, u} (pair X Y)
ht : IsLimit t
⊢ HAdd.hAdd (α := BinaryBicone.pt (BinaryBicone.ofLimitCone ht) ⟶ BinaryBicone.pt (BinaryBicone.ofLimitCone ht))
        (BinaryBicone.fst (BinaryBicone.ofLimitCone ht) ≫ BinaryBicone.inl (BinaryBicone.ofLimitCone ht))
        (BinaryBicone.snd (BinaryBicone.ofLimitCone ht) ≫ BinaryBicone.inr (BinaryBicone.ofLimitCone ht)) ≫
      BinaryFan.snd t =
    𝟙 (BinaryBicone.pt (BinaryBicone.ofLimitCone ht)) ≫ BinaryFan.snd t

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryProduct.{v, u} X Y
⊢ HasBinaryBiproduct.{v, u} X Y

Tactic:
HasBinaryBiproduct.mk
    { bicone := _
      isBilimit := binaryBiconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

Premises used: CategoryTheory.Limits.BinaryBicone.ofLimitCone, CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.Limits.HasBinaryBiproduct.mk, CategoryTheory.Limits.BinaryBiproductData.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryProducts.{v, u} C
⊢ HasBinaryBiproducts.{v, u} C

Tactic:
{ has_binary_biproduct := fun X Y => HasBinaryBiproduct.of_hasBinaryProduct X Y }

Premises used: CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct, CategoryTheory.Limits.HasBinaryBiproducts.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
x : ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.fst = NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 X) 0)) j
⊢ t.fst = BinaryCofan.IsColimit.desc ht (𝟙 X) 0

Tactic:
apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.BinaryCofan.mk, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (𝟙 X) 0))
    (t.toCocone.ι.app { as := WalkingPair.left } ≫ t.fst)
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 X) 0)) { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (𝟙 X) 0))
    (t.toCocone.ι.app { as := WalkingPair.right } ≫ t.fst)
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 X) 0)) { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
x : ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.snd = NatTrans.app (Cocone.ι (BinaryCofan.mk 0 (𝟙 Y))) j
⊢ t.snd = BinaryCofan.IsColimit.desc ht 0 (𝟙 Y)

Tactic:
apply ht.uniq (BinaryCofan.mk 0 (𝟙 Y))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.BinaryCofan.mk, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk 0 (𝟙 Y)))
    (t.toCocone.ι.app { as := WalkingPair.left } ≫ t.snd)
    (NatTrans.app (Cocone.ι (BinaryCofan.mk 0 (𝟙 Y))) { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk 0 (𝟙 Y)))
    (t.toCocone.ι.app { as := WalkingPair.right } ≫ t.snd)
    (NatTrans.app (Cocone.ι (BinaryCofan.mk 0 (𝟙 Y))) { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
BinaryCofan.IsColimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
refine_1 : BinaryCofan.inl t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inl t.toCocone ≫ 𝟙 t.pt
refine_2 : BinaryCofan.inr t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inr t.toCocone ≫ 𝟙 t.pt
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
refine BinaryCofan.IsColimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ BinaryCofan.inl t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inl t.toCocone ≫ 𝟙 t.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ BinaryCofan.inr t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inr t.toCocone ≫ 𝟙 t.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cocone.{0, v, 0, u} (pair X Y)
ht : IsColimit t
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
    (t.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
    ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
    (t.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
    ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.right })
⊢ t.ι.app j ≫ Iso.hom (Iso.refl t.pt) = (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cocone.{0, v, 0, u} (pair X Y)
ht : IsColimit t
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
    (t.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
    ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cocone.{0, v, 0, u} (pair X Y)
ht : IsColimit t
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
    (t.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
    ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ HasBinaryBiproduct.{v, u} X Y

Tactic:
HasBinaryBiproduct.mk
    { bicone := _
      isBilimit := binaryBiconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.BinaryBicone.ofColimitCocone, CategoryTheory.Limits.pair, CategoryTheory.Limits.HasBinaryBiproduct.mk, CategoryTheory.Limits.BinaryBiproductData.mk, CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
⊢ HasBinaryBiproducts.{v, u} C

Tactic:
{ has_binary_biproduct := fun X Y => HasBinaryBiproduct.of_hasBinaryCoproduct X Y }

Premises used: CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct, CategoryTheory.Limits.HasBinaryBiproducts.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
h₀ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
h₁ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd
h₂ :
  (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
h₃ :
  (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
    (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd
⊢ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr) = 𝟙 (biprod.{v, u} X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
⊢ (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
⊢ (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
⊢ (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
⊢ (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
    (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : T ⟶ X
g : T ⟶ Y
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) fst =
    HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) snd =
    HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ snd
⊢ lift f g = HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) fst =
    HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ fst

Tactic:
simp [add_comp]

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) snd =
    HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ snd

Tactic:
simp [add_comp]

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : X ⟶ T
g : Y ⟶ T
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) inl (desc f g) =
    inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) inr (desc f g) =
    inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
⊢ desc f g = HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) inl (desc f g) =
    inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)

Tactic:
simp