-- 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 : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
rw :
  e.f i ≫ f.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 : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₁ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X 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 : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₂ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₃ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
        (e.f i ≫ (prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom) +
      (e ≫ g).f i
rw₄ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
        (e.f i ≫ (prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom) +
      e.f i ≫ g.f i
⊢ (e ≫ f).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 : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
have rw₅ : e.f i ≫
      HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
    e.f i ≫ g.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
      (e.f i ≫ (prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom) +
    e.f i ≫ g.f i
Tactic: rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f,
    Preadditive.comp_add, Preadditive.comp_add]