-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma contractible_distinguished (X : HomotopyCategory C (ComplexShape.up ℤ)) :
    Pretriangulated.contractibleTriangle X ∈ distinguishedTriangles C

Proof state:
case mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
⊢ contractibleTriangle { as := X } ∈ distinguishedTriangles C

Tactic:
refine ⟨_, _, 𝟙 X, ⟨?_⟩⟩

Result:
case mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
⊢ contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ 0 ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map (𝟙 { as := X }) =
    h.isoZero.inv ≫
      (quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle (𝟙 X)).mor₃ ≫
        ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app X

Tactic:
ext

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ (contractibleTriangle { as := X }).mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl (contractibleTriangle { as := X }).obj₁).hom =
    h.isoZero.symm.hom ≫ (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₃

Tactic:
dsimp

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ 0 ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map (𝟙 { as := X }) =
    h.isoZero.inv ≫
      (quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle (𝟙 X)).mor₃ ≫
        ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomotopyCategory C (ComplexShape.up ℤ)
⊢ contractibleTriangle X ∈ distinguishedTriangles C

Tactic:
obtain ⟨X⟩ := X

Result:
case mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
⊢ contractibleTriangle { as := X } ∈ distinguishedTriangles C

Proof state:
case mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)

Tactic:
exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) h.isoZero.symm
  (by simp) (h.eq_of_tgt _ _) (by dsimp; ext)

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ (contractibleTriangle { as := X }).mor₁ ≫ (Iso.refl (contractibleTriangle { as := X }).obj₂).hom =
    (Iso.refl (contractibleTriangle { as := X }).obj₁).hom ≫ (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₁

Tactic:
simp

Result:
no goals

Proof state:
case mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
⊢ contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)

Tactic:
have h := (isZero_quotient_obj_iff _).2 ⟨CochainComplex.mappingCone.homotopyToZeroOfId X⟩

Result:
case mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)