C : Type u
inst✝⁹ : Category C
inst✝⁸ : HasZeroObject C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroObject D
inst✝² : HasShift D ℤ
inst✝¹ : Preadditive D
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor D n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
H₂ : Triangle.rotate (Triangle.rotate T) ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftEquiv C 1).functor.map T.mor₁ = 0
C : Type u
inst✝⁹ : Category C
inst✝⁸ : HasZeroObject C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroObject D
inst✝² : HasShift D ℤ
inst✝¹ : Preadditive D
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor D n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftEquiv C 1).functor.map T.mor₁ = 0
have H₂ := rot_of_dist_triangle C T.rotate (rot_of_dist_triangle C T H)
no goals
C : Type u
inst✝⁹ : Category C
inst✝⁸ : HasZeroObject C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroObject D
inst✝² : HasShift D ℤ
inst✝¹ : Preadditive D
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor D n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
H₂ : Triangle.rotate (Triangle.rotate T) ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftEquiv C 1).functor.map T.mor₁ = 0
simpa using comp_dist_triangle_mor_zero₁₂ C T.rotate.rotate H₂