-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₁) i =
    HAdd.hAdd (α :=
        (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).X i ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).X i)
        (β :=
        (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).X i ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).X i)
        ((dNext i :
              (a :
                  (i j : ℤ) →
                    ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K).X i ⟶
                      ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L).X j) →
                ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K).X i ⟶
                  ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L).X i)
            fun (x x_1 : ℤ) ↦
            HSMul.hSMul (β := K.X (x + { as := n : Discrete ℤ }.as) ⟶ L.X (x_1 + { as := n : Discrete ℤ }.as))
              n.negOnePow (h.hom (x + { as := n : Discrete ℤ }.as) (x_1 + { as := n : Discrete ℤ }.as)) :
          (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).X i ⟶
            (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).X i)
        ((prevD i :
              (a :
                  (i j : ℤ) →
                    ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K).X i ⟶
                      ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L).X j) →
                ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K).X i ⟶
                  ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L).X i)
            fun (x x_1 : ℤ) ↦
            HSMul.hSMul (β := K.X (x + { as := n : Discrete ℤ }.as) ⟶ L.X (x_1 + { as := n : Discrete ℤ }.as))
              n.negOnePow (h.hom (x + { as := n : Discrete ℤ }.as) (x_1 + { as := n : Discrete ℤ }.as)) :
          (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).X i ⟶
            (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).X i) +
      HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₂) i
have rw : HomologicalComplex.Hom.f
    (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₁) i =
  (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).d i (i + 1) ≫
        HSMul.hSMul (β := K.X (i + 1 + { as := n : Discrete ℤ }.as) ⟶ L.X (i + { as := n : Discrete ℤ }.as)) n.negOnePow
          (h.hom (i + 1 + { as := n : Discrete ℤ }.as) (i + { as := n : Discrete ℤ }.as)) +
      HSMul.hSMul (β := K.X (i + { as := n : Discrete ℤ }.as) ⟶ L.X (i - 1 + { as := n : Discrete ℤ }.as)) n.negOnePow
          (h.hom (i + { as := n : Discrete ℤ }.as) (i - 1 + { as := n : Discrete ℤ }.as)) ≫
        (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).d (i - 1) i +
    HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₂) i
Tactic: rw [dNext_eq _ (show (ComplexShape.up ℤ).Rel i (i + 1) by simp),
      prevD_eq _ (show (ComplexShape.up ℤ).Rel (i - 1) i by simp)]