case w
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).symm.hom = (shiftComm X j i).hom
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).symm = shiftComm X j i
ext
no goals
case w
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).symm.hom = (shiftComm X j i).hom
exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X