-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
P : ProjectiveResolution.{v, u} Y
Q : ProjectiveResolution.{v, u} Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
rw :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      (P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
rw₁ :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
              (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
              (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
rw₂ :
  HSub.hSub (α :=
      P.complex.X 1 ⟶
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).X₃)
      (P.complex.d 1 0 ≫ f.f 0)
      (P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
              (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
              (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g) =
    0
rw₃ :
  HSub.hSub (α :=
      P.complex.X 1 ⟶
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).X₃)
      (P.complex.d 1 0 ≫ f.f 0) (P.complex.d 1 0 ≫ f.f 0) =
    0
⊢ (f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
have rw₄ : Eq.{v + 1} (α :=
  P.complex.X 1 ⟶
    (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
        Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
        (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).X₃)
  0 0
Tactic: rw [Preadditive.sub_comp, assoc, HomologicalComplex.Hom.comm,
              liftHomotopyZeroZero_comp, sub_self]