[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.rotate X✝).mor₃ ≫ (shiftFunctor C 1).map f.hom₂ = (shiftFunctor C 1).map f.hom₁ ≫ (Triangle.rotate Y✝).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C 1).map X✝.mor₁) ≫ (shiftFunctor C 1).map f.hom₂ =
    (shiftFunctor C 1).map f.hom₁ ≫ (-(shiftFunctor C 1).map Y✝.mor₁)
[PROOFSTEP]
simp only [comp_neg, neg_comp, ← Functor.map_comp, f.comm₁]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.invRotate X✝).mor₁ ≫ f.hom₁ = (shiftFunctor C (-1)).map f.hom₃ ≫ (Triangle.invRotate Y✝).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C (-1)).map X✝.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom X✝.obj₁) ≫
      f.hom₁ =
    (shiftFunctor C (-1)).map f.hom₃ ≫
      (-(shiftFunctor C (-1)).map Y✝.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁)
[PROOFSTEP]
simp only [neg_comp, assoc, comp_neg, neg_inj, ← Functor.map_comp_assoc, ← f.comm₃]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (-1)).map X✝.mor₃ ≫
      NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom X✝.obj₁ ≫ f.hom₁ =
    (shiftFunctor C (-1)).map (X✝.mor₃ ≫ (shiftFunctor C 1).map f.hom₁) ≫
      NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁
[PROOFSTEP]
rw [Functor.map_comp, assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (-1)).map X✝.mor₃ ≫
      NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom X✝.obj₁ ≫ f.hom₁ =
    (shiftFunctor C (-1)).map X✝.mor₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁) ≫
        NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁
[PROOFSTEP]
erw [← NatTrans.naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (-1)).map X✝.mor₃ ≫
      (shiftFunctor C 1 ⋙ shiftFunctor C (-1)).map f.1 ≫
        NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁ =
    (shiftFunctor C (-1)).map X✝.mor₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁) ≫
        NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.invRotate X✝).mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map f.hom₃) =
    f.hom₂ ≫ (Triangle.invRotate Y✝).mor₃
[PROOFSTEP]
erw [← reassoc_of% f.comm₂, Category.assoc, ← NatTrans.naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ X✝.mor₂ ≫ (𝟭 C).map f.hom₃ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv Y✝.obj₃ =
    X✝.mor₂ ≫ f.hom₃ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv Y✝.3
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (rotate C)
[PROOFSTEP]
change IsEquivalence (triangleRotation C).functor
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (triangleRotation C).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (invRotate C)
[PROOFSTEP]
change IsEquivalence (triangleRotation C).inverse
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (triangleRotation C).inverse
[PROOFSTEP]
infer_instance
