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
P Q W X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
f : W ⟶ X
g : W ⟶ Y
inst_5 : Mono f
⊢ Mono (Y := biprod.{uC', uC} X Y) (lift f g)

Tactic:
mono_of_mono_fac <| biprod.lift_fst _ _

Premises used: CategoryTheory.Limits.biprod.lift_fst, CategoryTheory.mono_of_mono_fac
-- 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 W X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
f : W ⟶ X
g : W ⟶ Y
inst_5 : Mono g
⊢ Mono (Y := biprod.{uC', uC} X Y) (lift f g)

Tactic:
mono_of_mono_fac <| biprod.lift_snd _ _

Premises used: CategoryTheory.Limits.biprod.lift_snd, CategoryTheory.mono_of_mono_fac
-- 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 W X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
f : X ⟶ W
g : Y ⟶ W
inst_5 : Epi f
⊢ Epi (X := biprod.{uC', uC} X Y) (desc f g)

Tactic:
epi_of_epi_fac <| biprod.inl_desc _ _

Premises used: CategoryTheory.epi_of_epi_fac, CategoryTheory.Limits.biprod.inl_desc
-- 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 W X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
f : X ⟶ W
g : Y ⟶ W
inst_5 : Epi g
⊢ Epi (X := biprod.{uC', uC} X Y) (desc f g)

Tactic:
epi_of_epi_fac <| biprod.inr_desc _ _

Premises used: CategoryTheory.Limits.biprod.inr_desc, CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
f g : Z ⟶ biprod.{uC', uC} X Y
h₀ : f ≫ fst = g ≫ fst
h₁ : f ≫ snd = g ≫ snd
⊢ f = g

Tactic:
BinaryFan.IsLimit.hom_ext (BinaryBiproduct.isLimit X Y) h₀ h₁

Premises used: CategoryTheory.Limits.BinaryBiproduct.isLimit, CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
f g : biprod.{uC', uC} X Y ⟶ Z
h₀ : inl ≫ f = inl ≫ g
h₁ : inr ≫ f = inr ≫ g
⊢ f = g

Tactic:
BinaryCofan.IsColimit.hom_ext (BinaryBiproduct.isColimit X Y) h₀ h₁

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext, 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
h₁ :
  Eq.{uC' + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (Iso.hom (isoProd X Y) ≫ prod.fst))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.fst))
h₂ :
  Eq.{uC' + 1} (α := Y ⟶ X) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (Iso.hom (isoProd X Y) ≫ prod.fst))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.fst))
h₃ :
  Eq.{uC' + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (Iso.hom (isoProd X Y) ≫ prod.snd))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.snd))
h₄ :
  Eq.{uC' + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (Iso.hom (isoProd X Y) ≫ prod.snd))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.snd))
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ prod.{uC', uC} X Y) (Iso.hom (isoProd X Y)) (prod.lift fst snd)

Tactic:
ext
-- 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 (Iso.hom (isoProd X Y) ≫ prod.fst))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.fst))

Tactic:
simp [biprod.isoProd]

Premises used: CategoryTheory.Limits.biprod.isoProd
-- 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 (Iso.hom (isoProd X Y) ≫ prod.fst))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.fst))

Tactic:
simp [biprod.isoProd]

Premises used: CategoryTheory.Limits.biprod.isoProd
-- 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 (Iso.hom (isoProd X Y) ≫ prod.snd))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.snd))

Tactic:
simp [biprod.isoProd]

Premises used: CategoryTheory.Limits.biprod.isoProd
-- 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 (Iso.hom (isoProd X Y) ≫ prod.snd))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (CategoryStruct.comp (Y := prod.{uC', uC} X Y) (prod.lift fst snd) prod.snd))

Tactic:
simp [biprod.isoProd]

Premises used: CategoryTheory.Limits.biprod.isoProd
-- 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
h₀ :
  Eq.{uC' + 1} (α := prod.{uC', uC} X Y ⟶ X)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) fst : prod.{uC', uC} X Y ⟶ X)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift prod.fst prod.snd) fst : prod.{uC', uC} X Y ⟶ X)
h₁ :
  Eq.{uC' + 1} (α := prod.{uC', uC} X Y ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) snd : prod.{uC', uC} X Y ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift prod.fst prod.snd) snd : prod.{uC', uC} X Y ⟶ Y)
⊢ Eq.{uC' + 1} (α := prod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) (lift prod.fst prod.snd)

Tactic:
ext
-- 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} (α := prod.{uC', uC} X Y ⟶ X)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) fst : prod.{uC', uC} X Y ⟶ X)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift prod.fst prod.snd) fst : prod.{uC', uC} X Y ⟶ X)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- 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} (α := prod.{uC', uC} X Y ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) snd : prod.{uC', uC} X Y ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift prod.fst prod.snd) snd : prod.{uC', uC} X Y ⟶ Y)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- 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
h₁ :
  Eq.{uC' + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (coprod.inl ≫ Iso.inv (isoCoprod X Y)) fst)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inl (coprod.desc inl inr)) fst)
h₂ :
  Eq.{uC' + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (coprod.inl ≫ Iso.inv (isoCoprod X Y)) snd)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inl (coprod.desc inl inr)) snd)
h₃ :
  Eq.{uC' + 1} (α := Y ⟶ X) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (coprod.inr ≫ Iso.inv (isoCoprod X Y)) fst)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inr (coprod.desc inl inr)) fst)
h₄ :
  Eq.{uC' + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (coprod.inr ≫ Iso.inv (isoCoprod X Y)) snd)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inr (coprod.desc inl inr)) snd)
⊢ Eq.{uC' + 1} (α := coprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoCoprod X Y)) (coprod.desc inl inr)

Tactic:
ext
-- 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) (coprod.inl ≫ Iso.inv (isoCoprod X Y)) fst)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inl (coprod.desc inl inr)) fst)

Tactic:
simp [biprod.isoCoprod]

Premises used: CategoryTheory.Limits.biprod.isoCoprod
-- 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) (coprod.inl ≫ Iso.inv (isoCoprod X Y)) snd)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inl (coprod.desc inl inr)) snd)

Tactic:
simp [biprod.isoCoprod]

Premises used: CategoryTheory.Limits.biprod.isoCoprod
-- 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) (coprod.inr ≫ Iso.inv (isoCoprod X Y)) fst)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inr (coprod.desc inl inr)) fst)

Tactic:
simp [biprod.isoCoprod]

Premises used: CategoryTheory.Limits.biprod.isoCoprod
-- 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) (coprod.inr ≫ Iso.inv (isoCoprod X Y)) snd)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (CategoryStruct.comp (Y := coprod.{uC', uC} X Y) coprod.inr (coprod.desc inl inr)) snd)

Tactic:
simp [biprod.isoCoprod]

Premises used: CategoryTheory.Limits.biprod.isoCoprod
-- 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
h₀ :
  Eq.{uC' + 1} (α := X ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inl (Iso.hom (biprod.isoCoprod X Y)) :
      X ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inl (biprod.desc coprod.inl coprod.inr) :
      X ⟶ coprod.{uC', uC} X Y)
h₁ :
  Eq.{uC' + 1} (α := Y ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inr (Iso.hom (biprod.isoCoprod X Y)) :
      Y ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inr (biprod.desc coprod.inl coprod.inr) :
      Y ⟶ coprod.{uC', uC} X Y)
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ coprod.{uC', uC} X Y) (Iso.hom (biprod.isoCoprod X Y))
    (biprod.desc coprod.inl coprod.inr)

Tactic:
ext
-- 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 ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inl (Iso.hom (biprod.isoCoprod X Y)) :
      X ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inl (biprod.desc coprod.inl coprod.inr) :
      X ⟶ coprod.{uC', uC} X Y)

Tactic:
simp [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- 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 ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inr (Iso.hom (biprod.isoCoprod X Y)) :
      Y ⟶ coprod.{uC', uC} X Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) biprod.inr (biprod.desc coprod.inl coprod.inr) :
      Y ⟶ coprod.{uC', uC} X Y)

Tactic:
simp [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- 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₀ :
  CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map f g)) fst =
    CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) fst
h₁ :
  CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map f g)) snd =
    CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) snd
h₂ :
  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
h₃ :
  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
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g) (map' f g)

Tactic:
ext
-- 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} (α := W ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.left } :
          obj.{0, uC', 0, uC} (pair W X) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X))) { as := WalkingPair.left } ≫ f :
          obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone W X))))
              { as := WalkingPair.left : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) :
      W ⟶ Y)
    (f ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left }) :
      W ⟶ Y)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map f g)) fst =
    CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) fst

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.BinaryBicone.toCone_π_app_left, CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left, CategoryTheory.Limits.mapPair_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.{uC' + 1} (α := W ⟶ Y)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.left } :
          obj.{0, uC', 0, uC} (pair W X) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X))) { as := WalkingPair.left } ≫ f :
          obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone W X))))
              { as := WalkingPair.left : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) :
      W ⟶ Y)
    (f ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left }) :
      W ⟶ 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} (α := W ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.left })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X)))
            { as := WalkingPair.right : Discrete WalkingPair } ≫
          NatTrans.app (mapPair f g) { as := WalkingPair.right }) :
      W ⟶ Z)
    (f ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right }) :
      W ⟶ Z)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map f g)) snd =
    CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) snd

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.toCone_π_app_right, CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left, CategoryTheory.Limits.mapPair_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.{uC' + 1} (α := W ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.left })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X)))
            { as := WalkingPair.right : Discrete WalkingPair } ≫
          NatTrans.app (mapPair f g) { as := WalkingPair.right }) :
      W ⟶ Z)
    (f ≫
        CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
          (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left } :
            obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
          (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right }) :
      W ⟶ Z)

Tactic:
simp