-- 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
n : ℤ
⊢ Cochain.v
      (Cochain.ofHom
        (desc (inr φ) 0 (triangle φ).mor₃ ⋯ ≫
          lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯))
      n n ⋯ =
    (δ (-1) 0 (-Cochain.comp (snd (inr φ)) (Cochain.comp (snd φ) (inl (inr φ)) ⋯) ⋯) +
          Cochain.ofHom (𝟙 (mappingCone (G := mappingCone φ) (inr φ)))).v
      n n ⋯

Tactic:
simp only [Int.reduceNeg, Cochain.ofHom_comp, ofHom_desc, ofHom_lift, Cocycle.coe_neg,
        Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.comp_zero_cochain_v,
        shiftFunctor_obj_X', δ_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, Cochain.comp_add, inr_snd_assoc, neg_add_rev, Cochain.add_v, Cochain.neg_v,
        Cochain.comp_v _ _ (add_neg_cancel 1) n (n + 1) n rfl (by lia),
        Cochain.zero_cochain_comp_v, Cochain.ofHom_v, HomologicalComplex.id_f,
        ext_to_iff _ _ (n + 1) rfl, assoc, liftCochain_v_fst_v,
        (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) n (n + 1) rfl (n + 1) (by lia),
        shiftFunctor_obj_X, mul_one, sub_self, mul_zero, Int.zero_ediv, add_zero,
        shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, id_comp,
        Preadditive.add_comp, Preadditive.neg_comp, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero,
        neg_zero, neg_add_cancel_comm, ext_from_iff _ (n + 1) _ rfl, inl_v_descCochain_v_assoc,
        Cochain.zero_v, zero_comp, Preadditive.comp_neg, inl_v_snd_v_assoc,
        inr_f_descCochain_v_assoc, inr_f_snd_v_assoc, inl_v_triangle_mor₃_f_assoc, triangle_obj₁,
        Iso.refl_inv, inl_v_fst_v_assoc, inr_f_triangle_mor₃_f_assoc, inr_f_fst_v_assoc, and_self,
        liftCochain_v_snd_v,
        (inl φ).leftShift_v 1 0 (neg_add_cancel 1) n n (add_zero n) (n + 1) (by lia),
        Int.negOnePow_zero, inl_v_snd_v, inr_f_snd_v, zero_add, inl_v_descCochain_v,
        inr_f_descCochain_v, inl_v_triangle_mor₃_f, inr_f_triangle_mor₃_f, neg_add_cancel]

Premises used: neg_add_rev, CochainComplex.mappingCone.δ_inl, CochainComplex.mappingCone.inl_v_descCochain_v_assoc, CochainComplex.mappingCone.ofHom_desc, 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, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CochainComplex.HomComplex.Cochain.comp_add, CochainComplex.HomComplex.Cochain.neg_comp, CategoryTheory.Preadditive.comp_neg, CochainComplex.mappingCone.inr_snd_assoc, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CategoryTheory.Limits.comp_zero, CochainComplex.HomComplex.Cochain.zero_v, HomologicalComplex.id_f, 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, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, zero_add, one_smul, MulZeroClass.mul_zero, CochainComplex.mappingCone.inr_f_descCochain_v_assoc, CochainComplex.mappingCone.δ_snd, neg_add_cancel_comm, CochainComplex.mappingCone.inl_v_fst_v, CochainComplex.mappingCone.inr_f_descCochain_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, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.inr_f_snd_v_assoc, CategoryTheory.Preadditive.neg_comp, CochainComplex.mappingCone.inl_v_descCochain_v, 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