-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (CategoryStruct.comp (Y := Functor.obj F.leftDerivedToHomotopyCategory X)
        (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
        (Functor.map F.leftDerivedToHomotopyCategory f ≫ Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex)
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (CategoryStruct.comp (Y := Functor.obj F.leftDerivedToHomotopyCategory X)
        (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
          Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex)
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
rw₁ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (CategoryStruct.comp (Y := Functor.obj F.leftDerivedToHomotopyCategory X)
        (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
        (Functor.map F.leftDerivedToHomotopyCategory f ≫ Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex)
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
rw₂ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) ≫
        CategoryStruct.comp (Y := Functor.obj F.leftDerivedToHomotopyCategory Y)
          (Iso.inv (Q.isoLeftDerivedToHomotopyCategoryObj F)) (Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
      (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (Functor.map F.leftDerivedToHomotopyCategory f ≫ Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F))
    (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
      Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
have rw₃ : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
    (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
      P.complex)
    (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
  (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) ≫
      𝟙
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)) :
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
  (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
    (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
Tactic: rw [← cancel_epi (P.isoLeftDerivedToHomotopyCategoryObj F).inv, Iso.inv_hom_id_assoc,
      isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc f P Q φ comm F,
      Iso.inv_hom_id, comp_id]