no goals
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom
rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]