-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
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
F G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
obtain :
  ∀ (β : complex (projectiveResolution X) ⟶ P.complex)
    (hβ :
      Eq (α :=
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) (complex (projectiveResolution X)) ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex)
        (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) β) (Iso.hom P.iso)),
    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 (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
      (CategoryStruct.comp (Y := Functor.obj G.leftDerivedToHomotopyCategory X)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))))
          (Functor.map (G.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.hom P.iso)) :
        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 (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
      (CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex).as (r :=
                homotopic C (ComplexShape.down ℕ)))))
          (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.hom P.iso))
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) :
        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 (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
⊢ 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 (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
    (CategoryStruct.comp (Y := Functor.obj G.leftDerivedToHomotopyCategory X)
        (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))))
        (Functor.map (G.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.hom P.iso)) :
      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 (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ))
            ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex).as (r :=
              homotopic C (ComplexShape.down ℕ)))))
        (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.hom P.iso))
        (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) :
      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 (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))

Tactic:
obtain ⟨β, hβ⟩ := (HomotopyCategory.quotient _ _).map_surjective (iso P).hom

Premises used: CategoryTheory.ProjectiveResolution.iso, HomotopyCategory.quotient, CategoryTheory.Iso.hom, CategoryTheory.Functor.map_surjective