case h₀.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ map' f g) ≫ fst

case h₀.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ map' f g) ≫ snd

case h₁.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst

case h₁.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = map' f g
apply biprod.hom_ext' <;> apply biprod.hom_ext
case h₀.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.left } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.left } ≫ f =
    f ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.left } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.left }
case h₀.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ map' f g) ≫ fst
simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, biprod.inl_fst_assoc,
  Category.assoc, ← BinaryBicone.toCone_π_app_left, ← BinaryBiproduct.bicone_fst, ←
  BinaryBicone.toCocone_ι_app_left, ← BinaryBiproduct.bicone_inl]
case h₀.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ fst ≫ f = f ≫ inl ≫ fst
case h₀.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.left } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.left } ≫ f =
    f ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.left } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.left }
dsimp
no goals
case h₀.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ fst ≫ f = f ≫ inl ≫ fst
simp
case h₀.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.left } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.right } ≫
        (mapPair f g).app { as := WalkingPair.right } =
    f ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.left } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.right }
case h₀.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ map' f g) ≫ snd
simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, zero_comp, biprod.inl_snd_assoc,
  Category.assoc, ← BinaryBicone.toCone_π_app_right, ← BinaryBiproduct.bicone_snd, ←
  BinaryBicone.toCocone_ι_app_left, ← BinaryBiproduct.bicone_inl]
no goals
case h₀.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.left } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.right } ≫
        (mapPair f g).app { as := WalkingPair.right } =
    f ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.left } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.right }
simp
case h₁.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.right } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.left } ≫
        (mapPair f g).app { as := WalkingPair.left } =
    g ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.right } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.left }
case h₁.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst
simp only [mapPair_right, biprod.inr_fst_assoc, IsColimit.ι_map, IsLimit.map_π, zero_comp,
  Category.assoc, ← BinaryBicone.toCone_π_app_left, ← BinaryBiproduct.bicone_fst, ←
  BinaryBicone.toCocone_ι_app_right, ← BinaryBiproduct.bicone_inr]
no goals
case h₁.h₀
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.right } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.left } ≫
        (mapPair f g).app { as := WalkingPair.left } =
    g ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.right } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.left }
simp
case h₁.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.right } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.right } ≫ g =
    g ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.right } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.right }
case h₁.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd
simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π, biprod.inr_snd_assoc,
  Category.assoc, ← BinaryBicone.toCone_π_app_right, ← BinaryBiproduct.bicone_snd, ←
  BinaryBicone.toCocone_ι_app_right, ← BinaryBiproduct.bicone_inr]
no goals
case h₁.h₁
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBicone.toCocone (BinaryBiproduct.bicone W X)).ι.app { as := WalkingPair.right } ≫
      (BinaryBicone.toCone (BinaryBiproduct.bicone W X)).π.app { as := WalkingPair.right } ≫ g =
    g ≫
      (BinaryBicone.toCocone (BinaryBiproduct.bicone Y Z)).ι.app { as := WalkingPair.right } ≫
        (BinaryBicone.toCone (BinaryBiproduct.bicone Y Z)).π.app { as := WalkingPair.right }
simp