-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.map_eq_map' {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z]
    (f : W ⟶ Y) (g : X ⟶ Z) : biprod.map f g = biprod.map' f g

Proof state:
case h₁.h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Tactic:
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]

Result:
case h₁.h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.right } ≫ g =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.right }

Proof state:
case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫
        (mapPair f g).app { as := WalkingPair.left } =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }

Tactic:
simp

Result:
no goals

Proof state:
case h₁.h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.right } ≫ g =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Result:
no goals

Proof state:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Tactic:
simp

Result:
no goals

Proof state:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Tactic:
ext

Result:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Proof state:
case h₀.h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Tactic:
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]

Result:
case h₀.h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.left } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.right } ≫
        (mapPair f g).app { as := WalkingPair.right } =
    f ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.left } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.right }

Proof state:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.left } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫ f =
    f ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.left } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }

Tactic:
dsimp

Result:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Proof state:
case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Tactic:
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]

Result:
case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫
        (mapPair f g).app { as := WalkingPair.left } =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }

Proof state:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
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

Tactic:
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]

Result:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.left } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫ f =
    f ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.left } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }