-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
x x_1 : C
f₁ f₂ : x ⟶ x_1
h :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) x)
      (Functor.obj (singleFunctor C n) x_1))
    (CategoryTheory.Functor.map (singleFunctor C n) f₁) (CategoryTheory.Functor.map (singleFunctor C n) f₂)
eq₁ :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₁
eq₂ :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₂
rw :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₂
rw₁ :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1)
⊢ f₁ = f₂
have rw₂ : CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
    (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
      NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
  CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
    (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
      NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1)
Tactic: rw [← eq₁, ← eq₂, h]