awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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 ⟶ prod.{uC', uC} X Y) (Iso.hom (isoProd X Y)) (prod.lift fst snd)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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))
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ prod.{uC', uC} X Y) (Iso.hom (isoProd X Y)) (prod.lift fst snd)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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))
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ prod.{uC', uC} X Y) (Iso.hom (isoProd X Y)) (prod.lift fst snd)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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))
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ prod.{uC', uC} X Y) (Iso.hom (isoProd X Y)) (prod.lift fst snd)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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 ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) (lift prod.fst prod.snd)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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)
⊢ Eq.{uC' + 1} (α := prod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoProd X Y)) (lift prod.fst prod.snd)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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} (α := coprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoCoprod X Y)) (coprod.desc inl inr)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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)
⊢ Eq.{uC' + 1} (α := coprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoCoprod X Y)) (coprod.desc inl inr)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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)
⊢ Eq.{uC' + 1} (α := coprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoCoprod X Y)) (coprod.desc inl inr)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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)
⊢ Eq.{uC' + 1} (α := coprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (Iso.inv (isoCoprod X Y)) (coprod.desc inl inr)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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 ⟶ coprod.{uC', uC} X Y) (Iso.hom (biprod.isoCoprod X Y))
    (biprod.desc coprod.inl coprod.inr)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g) (map' f g)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g) (map' f g)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g) (map' f g)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g) (map' f g)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ 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
have 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)
Tactic: simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ 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
have 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)
Tactic: simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ 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
have h₁ : Eq.{uC' + 1} (α := X ⟶ Y)
  (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
      (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right })
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X)))
          { as := WalkingPair.left : Discrete WalkingPair } ≫
        NatTrans.app (mapPair f g) { as := WalkingPair.left }) :
    X ⟶ Y)
  (g ≫
      CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right } :
          obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))))
              { as := WalkingPair.right : Discrete WalkingPair })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.left }) :
    X ⟶ Y)
Tactic: simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
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
⊢ 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
have h₁ : Eq.{uC' + 1} (α := X ⟶ Z)
  (CategoryStruct.comp (Y := biprod.{uC', uC} W X)
      (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right } :
        obj.{0, uC', 0, uC} (pair W X) { as := WalkingPair.right : Discrete WalkingPair } ⟶
          obj.{0, uC', 0, uC}
            (obj (const (Discrete WalkingPair))
              (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone W X))))
            { as := WalkingPair.right : Discrete WalkingPair })
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone W X))) { as := WalkingPair.right } ≫ g :
        obj.{0, uC', 0, uC}
            (obj (const (Discrete WalkingPair))
              (Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone W X))))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair }) :
    X ⟶ Z)
  (g ≫
      CategoryStruct.comp (Y := biprod.{uC', uC} Y Z)
        (NatTrans.app (Cocone.ι (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right } :
          obj.{0, uC', 0, uC} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair } ⟶
            obj.{0, uC', 0, uC}
              (obj (const (Discrete WalkingPair))
                (Cocone.pt.{0, uC', 0, uC} (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z))))
              { as := WalkingPair.right : Discrete WalkingPair })
        (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z))) { as := WalkingPair.right }) :
    X ⟶ Z)
Tactic: simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := W ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map f g)) (f ≫ inl)
have rw : Eq (α := W ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inl (map' f g)) (f ≫ inl)
Tactic: rw [biprod.map_eq_map']