-- 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
n : ℤ
h : S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) = 𝟙 (S.X₁.X (n + 1))
h₁ :
  S.f.f (n + 1) ≫
      HSub.hSub (α := S.X₂.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
        (S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
        (ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₂ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (S.f.f (n + 1) ≫ S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₃ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      ((S.f ≫ S.g).f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₄ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (Hom.f 0 (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₅ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (0 ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₆ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n) 0
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₇ :
  Eq (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (-S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n)
    (-Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n)
h₈ h₉ :
  Eq (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (-Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) (-Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n)
⊢ S.f.f (n + 1) ≫
      HSub.hSub (α := S.X₂.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
        (S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
        (ShortComplex.Splitting.r (σ (n + 1)) ≫
          𝟙 (S.X₁.X (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n

Tactic:
rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]

Premises used: HomologicalComplex.zero_f, CategoryTheory.ShortComplex.zero, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.comp_f_assoc, zero_sub, CategoryTheory.Category.id_comp