case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ∀ (j : J), ι (F.obj ∘ f) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ (mapBiproduct F f).inv ≫ F.map (desc g) = desc fun j => F.map (g j)
apply biproduct.hom_ext'
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (F.obj ∘ f) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ∀ (j : J), ι (F.obj ∘ f) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
intro j
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (F.obj ∘ f) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
dsimp [Function.comp]
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
this : HasBiproduct fun j => F.obj (f j)
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
no goals
case w
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
this : HasBiproduct fun j => F.obj (f j)
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
simp only [mapBiproduct_inv, ← Category.assoc, biproduct.ι_desc ,← F.map_comp]