no goals
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ Hom.f ((single V c j).map f) j = (singleObjXSelf V c j A).hom ≫ f ≫ (singleObjXSelf V c j B).inv
simp