-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₂ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₃ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        ((I.cocomplex.d (n + 1) (n + 2) ≫ g') ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₄ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₅ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (g ≫
          CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (J.cocomplex.d n (n + 1))
            (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₆ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1)) (g ≫ 0) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₇ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1)) 0 -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₈ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₉ : Eq.{v + 1} (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) 0 0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]