-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f)))
    (CategoryStruct.comp (Y :=
        Functor.obj (quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (mappingCone f)))
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          ((mappingCone.triangle g).mor₃ ≫
            CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (mappingCone.inr f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f)) ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (𝟙 (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f))))
    (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
          (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g)) :
        Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
          Functor.obj (quotient C (ComplexShape.up ℤ))
            (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
            (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
                (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f) :
        Functor.obj (quotient C (ComplexShape.up ℤ))
            (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f))))
have rw : Eq (α :=
  Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
    Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f)))
  (CategoryStruct.comp (Y :=
    Functor.obj (quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (mappingCone f)))
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
      ((mappingCone.triangle g).mor₃ ≫
        CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
          (mappingCone.inr f)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f)))
  (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
      (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
        (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
            (mappingCone.map f (f ≫ g) (𝟙 X₁) g sorry : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f))
Tactic: rw [CategoryTheory.Functor.map_id, comp_id, ← Functor.map_comp_assoc]