-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
r_f :
  ShortComplex.Splitting.r (σ (p + 1 + 1)) ≫ S.f.f (p + 1 + 1) =
    𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1))
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
simp :
  -ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1) =
    -S.X₃.d (p + 1) (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)) -
      HSub.hSub (α := S.X₃.X (p + 1) ⟶ S.X₂.X (p + 1 + 1))
        (ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1) ≫ 𝟙 (S.X₂.X (p + 1 + 1)))
        (ShortComplex.Splitting.s (σ (p + 1)) ≫
          S.X₂.d (p + 1) (p + 1 + 1) ≫ S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)))
⊢ Eq (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
    (Iso.hom (mappingConeHomOfDegreewiseSplitXIso S σ p (p + 1) ⋯) ≫
        HSMul.hSMul (α := ℤˣ) (β := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1 + 1)) (-1) (S.X₂.d (p + 1) (p + 1 + 1)) :
      (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
    ((mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫
        Iso.hom (mappingConeHomOfDegreewiseSplitXIso S σ (p + 1) (p + 1 + 1) ⋯) :
      (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))

Tactic:
simp only [mappingConeHomOfDegreewiseSplitXIso, mappingCone.ext_from_iff _ _ _ rfl,
      mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by linarith) (by lia),
      cocycleOfDegreewiseSplit, r_f, Int.reduceNeg, Cochain.ofHom_v, sub_comp, assoc,
      Hom.comm, comp_sub, mappingCone.inl_v_fst_v_assoc, mappingCone.inl_v_snd_v_assoc,
      shiftFunctor_obj_X', zero_comp, sub_zero, homOfDegreewiseSplit_f,
      mappingCone.inr_f_fst_v_assoc, comp_zero, zero_sub, mappingCone.inr_f_snd_v_assoc,
      neg_neg, mappingCone.inr_f_d_assoc, shiftFunctor_obj_d',
      Int.negOnePow_one, neg_comp, sub_neg_eq_add, zero_add, and_true,
      Units.neg_smul, one_smul, comp_neg, ShortComplex.map_X₂, eval_obj, Cocycle.mk_coe,
      Cochain.mk_v]

Premises used: CochainComplex.mappingCone.inr_f_d_assoc, CategoryTheory.Category.assoc, CochainComplex.cocycleOfDegreewiseSplit, and_true, sub_zero, CategoryTheory.ShortComplex.map_X₂, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, CochainComplex.mappingCone.ext_from_iff, neg_neg, CochainComplex.HomComplex.Cochain.ofHom_v, Int.negOnePow_one, HomologicalComplex.eval_obj, CochainComplex.mappingCone.inl_v_snd_v_assoc, zero_add, one_smul, CochainComplex.homOfDegreewiseSplit_f, Units.neg_smul, CochainComplex.mappingCone.inr_f_fst_v_assoc, CochainComplex.mappingCone.inl_v_d_assoc, HAdd.hAdd, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.inr_f_snd_v_assoc, CategoryTheory.Preadditive.neg_comp, CochainComplex.mappingConeHomOfDegreewiseSplitXIso, CochainComplex.shiftFunctor_obj_d', CategoryTheory.Limits.zero_comp, OfNat.ofNat, CochainComplex.HomComplex.Cochain.mk_v, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.Hom.comm, CochainComplex.mappingCone.inl_v_fst_v_assoc, sub_neg_eq_add, CochainComplex.HomComplex.Cocycle.mk_coe, CategoryTheory.Preadditive.sub_comp, rfl, zero_sub