-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂))
    ((CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₁) ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a))
    (CategoryStruct.comp (Y := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₂).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₂ :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂)))
have rw : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
    Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂))
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₁ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a))
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
    CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₂)
Tactic: rw [← Functor.map_comp_assoc, triangleMapOfHomotopy_comm₃, Functor.map_comp, assoc, assoc]