-- 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
n : ℕ
rw :
  (Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f) ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
    CategoryStruct.comp (Y := (F.leftDerived n).obj Y)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          φ ≫
        Iso.inv (Q.isoLeftDerivedObj F n))
      (Iso.hom (Q.isoLeftDerivedObj F n))
rw₁ :
  Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
    CategoryStruct.comp (Y := (F.leftDerived n).obj Y)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          φ ≫
        Iso.inv (Q.isoLeftDerivedObj F n))
      (Iso.hom (Q.isoLeftDerivedObj F n))
⊢ Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ ≫
      Iso.inv (Q.isoLeftDerivedObj F n)
have rw₂ : Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
  CategoryStruct.comp (Y :=
    Functor.obj
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
      Q.complex)
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ :
      Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          P.complex ⟶
        Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          Q.complex)
    (CategoryStruct.comp (Y := (F.leftDerived n).obj Y) (Iso.inv (Q.isoLeftDerivedObj F n))
        (Iso.hom (Q.isoLeftDerivedObj F n)) :
      Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          Q.complex ⟶
        Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex))
Tactic: rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom, assoc, assoc,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]