Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: case h₀.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inl ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.fst =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst

pp: case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inl ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.snd =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd

pp: case h₁.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inr ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.fst =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst

pp: case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inr ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.snd =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd

Tactic:
<;>

Goal state after:
case h₀.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inl ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.fst =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst

case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inl ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.snd =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd

case h₁.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inr ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.fst =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst

case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : F.PreservesZeroMorphisms
⊢ (biprod.inr ≫ F.biprodComparison' X Y ≫ F.biprodComparison X Y) ≫ biprod.snd =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd