-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
rw :
  e.f i ≫ g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
rw₁ :
  (HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
          ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
          ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) +
        f.f i) ≫
      g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
rw₂ :
  (HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
          ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
          ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) +
        f.f i) ≫
      g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j :
          C.X i ⟶ E.X i) +
      (f ≫ g).f i
rw₃ :
  (HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
          ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
          ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) +
        f.f i) ≫
      g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i) +
      (f ≫ g).f i
rw₄ :
  HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
          ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
          ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) ≫
        g.f i +
      f.f i ≫ g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i) +
      (f ≫ g).f i
rw₅ :
  HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
          ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
          ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) ≫
        g.f i +
      f.f i ≫ g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i) +
      f.f i ≫ g.f i
⊢ (e ≫ g).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
have rw₆ : HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i) +
    f.f i ≫ g.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i) +
    f.f i ≫ g.f i
Tactic: rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp,
    comp_f, Preadditive.add_comp]