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) → W ⟶ f j
⊢ ∀ (j : J), (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (F.obj ∘ f) j = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) 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) → W ⟶ f j
⊢ F.map (lift g) ≫ (mapBiproduct F f).hom = lift 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) → W ⟶ f j
j' : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (F.obj ∘ f) j' = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) 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) → W ⟶ f j
⊢ ∀ (j : J), (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (F.obj ∘ f) j = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) 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) → W ⟶ f j
j' : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j' =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) 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) → W ⟶ f j
j' : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (F.obj ∘ f) j' = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) 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) → W ⟶ f j
j' : J
this : HasBiproduct fun j => F.obj (f j)
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j' =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) 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) → W ⟶ f j
j' : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j' =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) 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) → W ⟶ f j
j' : J
this : HasBiproduct fun j => F.obj (f j)
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j' =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j'
simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]