-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
lemma mappingConeCompTriangleh_distinguished :
    (mappingConeCompTriangleh f g) ∈
      distTriang (HomotopyCategory C (ComplexShape.up ℤ))

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (quotient C (ComplexShape.up ℤ)).map
        ((mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
      ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f) =
    (quotient C (ComplexShape.up ℤ)).map
        ((mappingConeCompHomotopyEquiv f g).hom ≫ (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃) ≫
      ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f)

Tactic:
congr 2

Result:
case e_a.e_a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f) =
    (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ mappingConeCompTriangleh f g ≅ mappingCone.triangleh (mappingConeCompTriangle f g).mor₁

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (isoOfHomotopyEquiv
  (mappingConeCompHomotopyEquiv f g)) (by aesop_cat) (by simp) ?_

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl (mappingConeCompTriangleh f g).obj₁).hom =
    (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).hom ≫
      (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₃

Proof state:
case e_a.e_a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f) =
    (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃

Tactic:
exact (mappingConeCompHomotopyEquiv_comm₂ f g).symm

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl (mappingConeCompTriangleh f g).obj₁).hom =
    (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).hom ≫
      (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₃

Tactic:
dsimp [mappingConeCompTriangleh]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ ((quotient C (ComplexShape.up ℤ)).map
          ((mappingCone.triangle g).mor₃ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
        ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f)) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (𝟙 ((quotient C (ComplexShape.up ℤ)).obj (mappingCone f))) =
    (quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
      (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃ ≫
        ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ ((quotient C (ComplexShape.up ℤ)).map
          ((mappingCone.triangle g).mor₃ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
        ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f)) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (𝟙 ((quotient C (ComplexShape.up ℤ)).obj (mappingCone f))) =
    (quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
      (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃ ≫
        ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f)

Tactic:
rw [CategoryTheory.Functor.map_id, comp_id, ← Functor.map_comp_assoc]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (quotient C (ComplexShape.up ℤ)).map
        ((mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
      ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f) =
    (quotient C (ComplexShape.up ℤ)).map
        ((mappingConeCompHomotopyEquiv f g).hom ≫ (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃) ≫
      ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (mappingCone f)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₂ ≫ (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).hom =
    (Iso.refl (mappingConeCompTriangleh f g).obj₂).hom ≫ (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₁ ≫ (Iso.refl (mappingConeCompTriangleh f g).obj₂).hom =
    (Iso.refl (mappingConeCompTriangleh f g).obj₁).hom ≫ (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₁

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ mappingConeCompTriangleh f g ∈ distinguishedTriangles

Tactic:
refine ⟨_, _, (mappingConeCompTriangle f g).mor₁, ⟨?_⟩⟩

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst✝ : HasZeroObject C
⊢ mappingConeCompTriangleh f g ≅ mappingCone.triangleh (mappingConeCompTriangle f g).mor₁