-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
rw₁ :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₂ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₃ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
hc : p + 1 + -1 = p
rw₄ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
hc₁ : p + -1 = p - 1
hc₂ : p + 1 + -1 = p
rw₅ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
hc₃ : p + -1 = p - 1
hc₄ : p + 1 + -1 = p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p

Tactic:
rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]

Premises used: dif_pos, prevD_eq, dNext_eq