[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₁ ≫ T.mor₂ = 0
[PROOFSTEP]
obtain ⟨c, hc⟩ :=
  complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁) T.mor₁ rfl
[GOAL]
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C 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
[PROOFSTEP]
simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftEquiv C 1).functor.map T.mor₁ = 0
[PROOFSTEP]
have H₂ := rot_of_dist_triangle T.rotate (rot_of_dist_triangle T H)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C 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
[PROOFSTEP]
simpa using comp_dist_triangle_mor_zero₁₂ T.rotate.rotate H₂
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
obtain ⟨X', f', g', mem⟩ := distinguished_cocone_triangle g
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
X' : C
f' : Z ⟶ X'
g' : X' ⟶ (shiftFunctor C 1).obj Y
mem : Triangle.mk g f' g' ∈ distinguishedTriangles
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
exact ⟨_, _, _, inv_rot_of_dist_triangle _ mem⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
obtain ⟨Y', f', g', mem⟩ := distinguished_cocone_triangle h
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
let T' := (Triangle.mk h f' g').invRotate.invRotate
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
refine'
  ⟨T'.obj₂, ((shiftEquiv C (1 : ℤ)).unitIso.app X).hom ≫ T'.mor₁, T'.mor₂,
    isomorphic_distinguished _ (inv_rot_of_dist_triangle _ (inv_rot_of_dist_triangle _ mem)) _ _⟩
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h ≅
    Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
[PROOFSTEP]
exact
  Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
    (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₁ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₂ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom ≫
      (Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))).mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₃ ≫
      (shiftFunctor C 1).map ((shiftEquiv C 1).unitIso.app X).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom ≫
      (Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ h ≫ (shiftFunctor C 1).map (NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).inv X) =
    𝟙 Z ≫ h ≫ NatTrans.app (shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv ((shiftFunctor C 1).obj X)
[PROOFSTEP]
simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ :=
  complete_distinguished_triangle_morphism _ _ (rot_of_dist_triangle _ hT₁) (rot_of_dist_triangle _ hT₂) b c comm
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
[PROOFSTEP]
refine' ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨_, _⟩⟩
[GOAL]
case intro.intro.refine'_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ T₁.mor₁ ≫ b = (shiftFunctor C 1).preimage a ≫ T₂.mor₁
[PROOFSTEP]
apply (shiftFunctor C (1 : ℤ)).map_injective
[GOAL]
case intro.intro.refine'_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
[PROOFSTEP]
dsimp at ha₂ 
[GOAL]
case intro.intro.refine'_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (-(shiftFunctor C 1).map T₁.mor₁) ≫ (shiftFunctor C 1).map b = a ≫ (-(shiftFunctor C 1).map T₂.mor₁)
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
[PROOFSTEP]
rw [neg_comp, comp_neg, neg_inj] at ha₂ 
[GOAL]
case intro.intro.refine'_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
[PROOFSTEP]
simpa only [Functor.map_comp, Functor.image_preimage] using ha₂
[GOAL]
case intro.intro.refine'_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a) = c ≫ T₂.mor₃
[PROOFSTEP]
simpa only [Functor.image_preimage] using ha₁
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ :=
  complete_distinguished_triangle_morphism _ _ (inv_rot_of_dist_triangle _ hT₁) (inv_rot_of_dist_triangle _ hT₂)
    (c⟦(-1 : ℤ)⟧') a
    (by
      dsimp
      simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm, Functor.map_comp, shift_shift_neg',
        Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ (Triangle.invRotate T₁).mor₁ ≫ a = (shiftFunctor C (-1)).map c ≫ (Triangle.invRotate T₂).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ (-(shiftFunctor C (-1)).map T₁.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom T₁.obj₁) ≫
      a =
    (shiftFunctor C (-1)).map c ≫
      (-(shiftFunctor C (-1)).map T₂.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom T₂.obj₁)
[PROOFSTEP]
simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm, Functor.map_comp, shift_shift_neg', Functor.id_obj,
  assoc, Iso.inv_hom_id_app, comp_id]
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (Triangle.invRotate T₁).mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ (Triangle.invRotate T₂).mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a✝ ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
[PROOFSTEP]
refine' ⟨a, ⟨ha₁, _⟩⟩
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (Triangle.invRotate T₁).mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ (Triangle.invRotate T₂).mor₃
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂
[PROOFSTEP]
dsimp only [Triangle.invRotate, Triangle.mk] at ha₂ 
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (T₁.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₂.3
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂
[PROOFSTEP]
rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (T₁.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₂.3
⊢ T₁.mor₂ ≫ c ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₂.obj₃ =
    (T₁.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)
[PROOFSTEP]
simp only [shiftEquiv'_counitIso, shift_neg_shift', assoc, Iso.inv_hom_id_app_assoc]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ∈ distinguishedTriangles
[PROOFSTEP]
refine' isomorphic_distinguished _ (inv_rot_of_dist_triangle _ (contractible_distinguished X)) _ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ≅ Triangle.invRotate (contractibleTriangle X)
[PROOFSTEP]
exact
  Triangle.isoMk _ _ (Functor.mapZeroObject _).symm (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
    (by aesop_cat)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom =
    (Functor.mapZeroObject (shiftFunctor C (-1))).symm.hom ≫ (Triangle.invRotate (contractibleTriangle X)).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₂ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom ≫ (Triangle.invRotate (contractibleTriangle X)).mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₃ ≫ (shiftFunctor C 1).map (Functor.mapZeroObject (shiftFunctor C (-1))).symm.hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom ≫ (Triangle.invRotate (contractibleTriangle X)).mor₃
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles
[PROOFSTEP]
refine' isomorphic_distinguished _ (inv_rot_of_dist_triangle _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ≅ Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)
[PROOFSTEP]
exact
  Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
    (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₁ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₂ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom ≫
      (Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)).mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₃ ≫ (shiftFunctor C 1).map ((shiftEquiv C 1).unitIso.app X).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom ≫
      (Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ 𝟙 ((shiftFunctor C 1).obj X) ≫
      (shiftFunctor C 1).map (NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).inv X) =
    𝟙 ((shiftFunctor C 1).obj X) ≫
      𝟙 ((shiftFunctor C 1).obj X) ≫
        NatTrans.app (shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv ((shiftFunctor C 1).obj X)
[PROOFSTEP]
simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ ∃ g, f = T.mor₂ ≫ g
[PROOFSTEP]
obtain ⟨g, ⟨hg₁, _⟩⟩ :=
  complete_distinguished_triangle_morphism T _ hT (contractible_distinguished₁ X) 0 f (by aesop_cat)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ T.mor₁ ≫ f = 0 ≫ (Triangle.mk 0 (𝟙 X) 0).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (Triangle.mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (Triangle.mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (shiftFunctor C 1).map 0 = g ≫ (Triangle.mk 0 (𝟙 X) 0).mor₃
⊢ ∃ g, f = T.mor₂ ≫ g
[PROOFSTEP]
exact ⟨g, by simpa using hg₁.symm⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (Triangle.mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (Triangle.mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (shiftFunctor C 1).map 0 = g ≫ (Triangle.mk 0 (𝟙 X) 0).mor₃
⊢ f = T.mor₂ ≫ g
[PROOFSTEP]
simpa using hg₁.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ ∃ g, f = g ≫ T.mor₁
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, _⟩⟩ :=
  complete_distinguished_triangle_morphism₁ _ T (contractible_distinguished X) hT f 0 (by aesop_cat)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ (contractibleTriangle X).mor₂ ≫ 0 = f ≫ T.mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ ∃ g, f = g ≫ T.mor₁
[PROOFSTEP]
exact ⟨a, by simpa using ha₁⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ f = a ≫ T.mor₁
[PROOFSTEP]
simpa using ha₁
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ (shiftFunctor C 1).obj T.obj₁
hf : f ≫ (shiftFunctor C 1).map T.mor₁ = 0
⊢ f ≫ (Triangle.rotate (Triangle.rotate T)).mor₂ = 0
[PROOFSTEP]
aesop_cat
