no goals
ι : Type ?u.172926
V : Type u
inst✝⁶ : Category V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type ?u.173295
inst✝³ : Category W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ HomologicalComplex.X ((F ⋙ single W c j).obj X) j =
    HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) j
simp
no goals
ι : Type u_3
V : Type u
inst✝⁶ : Category V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ Hom.f ((singleMapHomologicalComplex F c j).inv.app X) j =
    eqToHom (_ : (if j = j then F.obj X else 0) = F.obj (if j = j then X else 0))
simp [singleMapHomologicalComplex]