case intro
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
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ 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₁ ≫ T.mor₂ = 0
obtain ⟨c, hc⟩ :=
  complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁)
    T.mor₁ rfl
no goals
case intro
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
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0
simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm