[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ Nonempty
    (Octahedron (_ : 𝟙 X ≫ 𝟙 X = 𝟙 X) (_ : contractibleTriangle X ∈ distinguishedTriangles)
      (_ : contractibleTriangle X ∈ distinguishedTriangles) (_ : contractibleTriangle X ∈ distinguishedTriangles))
[PROOFSTEP]
refine'
  ⟨⟨0, 0, _, _, _, _,
      isomorphic_distinguished _ (contractible_distinguished (0 : C)) _
        (Triangle.isoMk _ _ (by rfl) (by rfl) (by rfl))⟩⟩
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₁ ≅ (contractibleTriangle 0).obj₁
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₂ ≅ (contractibleTriangle 0).obj₂
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₃ ≅ (contractibleTriangle 0).obj₃
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
case refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
case refine'_3
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
case refine'_4
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ (shiftFunctor C 1).map (𝟙 X) = 0 ≫ 0
[PROOFSTEP]
all_goals apply Subsingleton.elim
[GOAL]
case refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_3
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_4
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ (shiftFunctor C 1).map (𝟙 X) = 0 ≫ 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁ ≫ u₂₃ = 𝟙 X₁ ≫ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃
[PROOFSTEP]
rw [id_comp, comm]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫ (shiftFunctor C 1).map (𝟙 X₁) = h.m₁ ≫ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ w₁₂ ≫ (shiftFunctor C 1).map (𝟙 X₁) = h.m₁ ≫ w₁₃
[PROOFSTEP]
simpa only [Functor.map_id, comp_id] using h.comm₂.symm
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁ ≫ 𝟙 X₃ = u₁₂ ≫ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
[PROOFSTEP]
rw [comp_id, comm]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂ ≫ h.m₃ = 𝟙 X₃ ≫ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₂
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ v₁₃ ≫ h.m₃ = 𝟙 X₃ ≫ v₂₃
[PROOFSTEP]
rw [id_comp, h.comm₃]
