[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : Additive F
J✝ : Type
inst✝ : Fintype J✝
f✝ : J✝ → C
b✝ : Bicone f✝
hb : Bicone.IsBilimit b✝
⊢ (Finset.sum Finset.univ fun j => Bicone.π (mapBicone F b✝) j ≫ Bicone.ι (mapBicone F b✝) j) = 𝟙 (mapBicone F b✝).pt
[PROOFSTEP]
simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : Additive F
J✝ : Type
inst✝ : Fintype J✝
f✝ : J✝ → C
b✝ : Bicone f✝
hb : Bicone.IsBilimit b✝
⊢ (Finset.sum Finset.univ fun x => F.map (Bicone.π b✝ x ≫ Bicone.ι b✝ x)) = 𝟙 (mapBicone F b✝).pt
[PROOFSTEP]
erw [← F.map_sum, ← F.map_id, IsBilimit.total hb]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g
[PROOFSTEP]
rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod, ← biprod.mapBiprod_hom_desc, Category.assoc,
  Iso.inv_hom_id_assoc, F.map_id, biprod.add_eq_lift_id_desc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.46335, u_1} C
inst✝³ : Category.{?u.46339, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
e : C ≌ D
inst✝ : Functor.Additive e.functor
f g : D
f✝ g✝ : f ⟶ g
⊢ e.functor.map (e.inverse.map (f✝ + g✝)) = e.functor.map (e.inverse.map f✝ + e.inverse.map g✝)
[PROOFSTEP]
simp
