-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
p : ℤ
⊢ Cochain.v
      (Cochain.ofHom
        ((triangle φ).mor₃ ≫
          lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
            (-Cochain.leftShift (inl φ) 1 0 rotateHomotopyEquiv._proof_9) ⋯))
      p p ⋯ =
    HAdd.hAdd (α := (mappingCone φ).X p ⟶ (mappingCone (G := mappingCone φ) (inr φ)).X p)
      (Cochain.v (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) ⋯)) p p ⋯)
      (Cochain.v (Cochain.ofHom (inr (inr φ))) p p ⋯)

Tactic:
simp only [Int.reduceNeg, Cochain.ofHom_comp, ofHom_lift, Cocycle.coe_neg,
          Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.comp_zero_cochain_v,
          shiftFunctor_obj_X', Cochain.ofHom_v, δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
          δ_inl, Int.negOnePow_neg, Int.negOnePow_one, δ_snd, Cochain.neg_comp,
          Cochain.comp_assoc_of_second_is_zero_cochain, smul_neg, Units.neg_smul, one_smul, neg_neg,
          neg_add_rev, Cochain.add_v, Cochain.neg_v,
          Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p rfl (by lia),
          Cochain.zero_cochain_comp_v, ext_from_iff _ _ _ rfl, inl_v_triangle_mor₃_f_assoc,
          triangle_obj₁, shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
          Iso.refl_inv, Preadditive.neg_comp, id_comp, Preadditive.comp_add, Preadditive.comp_neg,
          inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, neg_zero, add_zero, ext_to_iff _ _ _ rfl,
          liftCochain_v_fst_v,
          (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia), mul_one,
          sub_self, mul_zero, Int.zero_ediv, Iso.refl_hom, Preadditive.add_comp, assoc, inl_v_fst_v,
          comp_id, inr_f_fst_v, comp_zero, liftCochain_v_snd_v,
          (inl φ).leftShift_v 1 0 (neg_add_cancel 1) p p (add_zero p) (p + 1) (by lia),
          Int.negOnePow_zero, inl_v_snd_v, inr_f_snd_v, zero_add, and_self,
          inr_f_triangle_mor₃_f_assoc, inr_f_fst_v_assoc, inr_f_snd_v_assoc, neg_add_cancel]

Premises used: neg_add_rev, CochainComplex.mappingCone.δ_inl, CategoryTheory.Category.assoc, add_neg_cancel, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.mappingCone.liftCochain_v_snd_v, CochainComplex.HomComplex.δ_neg, sub_self, and_self, CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CochainComplex.HomComplex.Cochain.neg_v, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CochainComplex.HomComplex.Cochain.neg_comp, CategoryTheory.Preadditive.comp_neg, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingCone.ext_from_iff, CochainComplex.HomComplex.Cocycle.coe_neg, neg_neg, smul_neg, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.mappingCone.inr_f_snd_v, Int.negOnePow_neg, CochainComplex.mappingCone.ofHom_lift, CochainComplex.mappingCone.ext_to_iff, Int.negOnePow_one, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.liftCochain_v_fst_v, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, CochainComplex.mappingCone.inl_v_snd_v_assoc, zero_add, one_smul, MulZeroClass.mul_zero, CochainComplex.mappingCone.δ_snd, CochainComplex.mappingCone.inl_v_fst_v, CategoryTheory.Preadditive.add_comp, CochainComplex.HomComplex.Cochain.ofHom, CategoryTheory.Iso.refl_inv, Units.neg_smul, CochainComplex.mappingCone.inr_f_fst_v_assoc, neg_add_cancel, HAdd.hAdd, Int.zero_ediv, Int.negOnePow_zero, CochainComplex.HomComplex.Cochain.leftShift_v, CategoryTheory.Preadditive.comp_add, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.inr_f_snd_v_assoc, CategoryTheory.Preadditive.neg_comp, CochainComplex.HomComplex.Cocycle.ofHom_coe, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CategoryTheory.Limits.zero_comp, CochainComplex.mappingCone.inl_v_snd_v, mul_one, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cocycle.leftShift_coe, neg_zero, CategoryTheory.Iso.refl_hom, CochainComplex.HomComplex.Cochain.add_v, CochainComplex.mappingCone.inl_v_fst_v_assoc, CochainComplex.HomComplex.δ_zero_cochain_comp, CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain, rfl, CochainComplex.mappingCone.triangle_obj₁, CochainComplex.mappingCone.inl, CategoryTheory.Category.id_comp, CochainComplex.HomComplex.Cochain.ofHom_comp