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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
⊢ Eq.{uC' + 1} (α :=
    Cone.pt.{0, uC', 0, uC} (F := parallelPair (X := biprod.{uC', uC} X Y) snd 0) (sndKernelFork X Y) ⟶
      biprod.{uC', uC} X Y)
    (Fork.ι (sndKernelFork X Y)) inl

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, 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} (α :=
    biprod.{uC', uC} X Y ⟶
      Cocone.pt.{0, uC', 0, uC} (F := parallelPair (X := X) (Y := biprod.{uC', uC} X Y) inl 0) (inlCokernelCofork X Y))
    (Cofork.π (inlCokernelCofork X Y)) snd

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- 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} (α :=
    biprod.{uC', uC} X Y ⟶
      Cocone.pt.{0, uC', 0, uC} (F := parallelPair (X := Y) (Y := biprod.{uC', uC} X Y) inr 0) (inrCokernelCofork X Y))
    (Cofork.π (inrCokernelCofork X Y)) fst

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op (biprod.{uC', uC} P Q) ⟶ op P) (Iso.hom (opIso P Q) ≫ fst) (Quiver.Hom.op inl)

Tactic:
lift_fst _ _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, Quiver.Hom.op, CategoryTheory.Limits.biprod.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op (biprod.{uC', uC} P Q) ⟶ op Q) (Iso.hom (opIso P Q) ≫ snd) (Quiver.Hom.op inr)

Tactic:
lift_snd _ _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.biprod.lift_snd, Quiver.Hom.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op P ⟶ op (biprod.{uC', uC} P Q)) (inl ≫ Iso.inv (opIso P Q)) (Quiver.Hom.op fst)

Tactic:
inl_desc _ _

Premises used: Quiver.Hom.op, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.biprod.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op Q ⟶ op (biprod.{uC', uC} P Q)) (inr ≫ Iso.inv (opIso P Q)) (Quiver.Hom.op snd)

Tactic:
inr_desc _ _

Premises used: Quiver.Hom.op, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.biprod.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op P ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
        op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)
h₁ :
  Eq.{uC' + 1} (α := op P ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
        op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)
⊢ Eq.{uC' + 1} (α := op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
      op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op P ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
        op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op P ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
        op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op Q ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
        op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)
h₁ :
  Eq.{uC' + 1} (α := op Q ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
        op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr snd)
⊢ Eq.{uC' + 1} (α := op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
      op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op Q ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
        op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op Q ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
        op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr snd)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op P ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)
h₁ :
  Eq.{uC' + 1} (α := op Q ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} (op P) (op Q) ⟶ op P)
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op P)
    (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op P ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op Q ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op P ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)
h₁ :
  Eq.{uC' + 1} (α := op Q ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr snd)
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
    (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op P ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op Q ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr snd)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- 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
⊢ HasKernel.{uC', uC} (C := C) (X := biprod.{uC', uC} X Y) biprod.fst

Tactic:
HasLimit.mk ⟨_, biprod.isKernelFstKernelFork X Y⟩

Premises used: CategoryTheory.Limits.biprod.isKernelFstKernelFork, 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 X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
⊢ HasKernel.{uC', uC} (C := C) (X := biprod.{uC', uC} X Y) biprod.snd

Tactic:
HasLimit.mk ⟨_, biprod.isKernelSndKernelFork X Y⟩

Premises used: CategoryTheory.Limits.biprod.isKernelSndKernelFork, 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 X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
⊢ HasCokernel.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) biprod.inl

Tactic:
HasColimit.mk ⟨_, biprod.isCokernelInlCokernelFork X Y⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.biprod.isCokernelInlCokernelFork
-- 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
⊢ HasCokernel.{uC', uC} (C := C) (X := Y) (Y := biprod.{uC', uC} X Y) biprod.inr

Tactic:
HasColimit.mk ⟨_, biprod.isCokernelInrCokernelFork X Y⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.biprod.isCokernelInrCokernelFork
-- 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
hY : IsZero.{uC', uC} Y
h₀ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.snd =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd
⊢ biprod.fst ≫ biprod.inl = 𝟙 (biprod.{uC', uC} X Y)

Tactic:
apply CategoryTheory.Limits.biprod.hom_ext

Premises used: CategoryTheory.Limits.biprod.hom_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 X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} Y
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst

Tactic:
simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_snd, CategoryTheory.Category.id_comp
-- 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
hY : IsZero.{uC', uC} Y
h₁ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ Y) 0 biprod.snd
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.snd =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd

Tactic:
simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_snd, CategoryTheory.Category.id_comp
-- 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
hY : IsZero.{uC', uC} Y
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ Y) 0 biprod.snd

Tactic:
apply hY.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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
hY : IsZero.{uC', uC} X
h₀ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.snd =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd
⊢ biprod.snd ≫ biprod.inr = 𝟙 (biprod.{uC', uC} X Y)

Tactic:
apply CategoryTheory.Limits.biprod.hom_ext

Premises used: CategoryTheory.Limits.biprod.hom_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 X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} X
h₀ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) 0 biprod.fst
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst

Tactic:
simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inr_snd, CategoryTheory.Category.id_comp
-- 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
hY : IsZero.{uC', uC} X
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.snd =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd

Tactic:
simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inr_snd, CategoryTheory.Category.id_comp
-- 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
hY : IsZero.{uC', uC} X
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) 0 biprod.fst

Tactic:
apply hY.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
mp : IsZero.{uC', uC} (biprod.{uC', uC} A B) → IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B
mpr : IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B → IsZero.{uC', uC} (biprod.{uC', uC} A B)
⊢ IsZero.{uC', uC} (biprod.{uC', uC} A B) ↔ IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
h : IsZero.{uC', uC} (biprod.{uC', uC} A B)
mp :
  ∀ (h : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0),
    Eq.{uC' + 1} (α := A ⟶ A) (𝟙 A) 0 ∧ Eq.{uC' + 1} (α := B ⟶ B) (𝟙 B) 0
⊢ IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B

Tactic:
simp only [IsZero.iff_id_eq_zero] at h ⊢

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
h : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
⊢ 𝟙 A = biprod.inl ≫ 𝟙 (biprod.{uC', uC} A B) ≫ biprod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
h : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
⊢ 𝟙 B = biprod.inr ≫ 𝟙 (biprod.{uC', uC} A B) ≫ biprod.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
h : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
⊢ Eq.{uC' + 1} (α := A ⟶ A) (𝟙 A) 0 ∧ Eq.{uC' + 1} (α := B ⟶ B) (𝟙 B) 0

Tactic:
simp only [show 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst by simp,
      show 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd by simp, h, zero_comp, comp_zero,
      and_self]

Premises used: and_self, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
mpr : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
⊢ IsZero.{uC', uC} (biprod.{uC', uC} A B)

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero