no goals
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
classical
  ext
  simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]
case w.w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
j✝¹ j✝ : J
⊢ (biproduct.ι (F.obj ∘ f) j✝¹ ≫ biproductComparison' F f ≫ biproductComparison F f) ≫ biproduct.π (F.obj ∘ f) j✝ =
    (biproduct.ι (F.obj ∘ f) j✝¹ ≫ 𝟙 (⨁ F.obj ∘ f)) ≫ biproduct.π (F.obj ∘ f) j✝
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
ext
no goals
case w.w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
j✝¹ j✝ : J
⊢ (biproduct.ι (F.obj ∘ f) j✝¹ ≫ biproductComparison' F f ≫ biproductComparison F f) ≫ biproduct.π (F.obj ∘ f) j✝ =
    (biproduct.ι (F.obj ∘ f) j✝¹ ≫ 𝟙 (⨁ F.obj ∘ f)) ≫ biproduct.π (F.obj ∘ f) j✝
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]