-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst_3 : K.IsKProjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
e_2 :
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)) =
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L)))
x : CohomologyClass K L n
h :
  ∀ (x : Cocycle K L n),
    Eq (α :=
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))
      (Function.comp (β :=
          Quiver.Hom (V := DerivedCategory C) (Functor.obj Q K)
            (Functor.obj (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n) L))
          (⇑(Iso.homCongr (Iso.app (Iso.symm (quotientCompQhIso C)) K)
                (Iso.trans (Y := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n ⋙ Q) L)
                  (Iso.app (Iso.symm (Functor.commShiftIso Q n)) L)
                  (Iso.app (Iso.symm (quotientCompQhIso C))
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))) :
            (a : Q.obj K ⟶ (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n).obj L) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
                  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))
          (Function.comp (β := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
            (⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) :
              (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
                ShiftedHom (Q.obj K) (Q.obj L) n)
            toSmallShiftedHom)
          (mk x) :
        Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
          (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))
      ((CategoryTheory.Functor.map Qh ∘
            (⇑toHom :
              (a : CohomologyClass K L n) →
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                    ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)))
          (mk x) :
        Quiver.Hom (V := DerivedCategory C)
          (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
          (Functor.obj Qh
            (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))))
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))
    (Function.comp (β :=
        Quiver.Hom (V := DerivedCategory C) (Functor.obj Q K)
          (Functor.obj (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n) L))
        (⇑(Iso.homCongr (Iso.app (Iso.symm (quotientCompQhIso C)) K)
              (Iso.trans (Y := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n ⋙ Q) L)
                (Iso.app (Iso.symm (Functor.commShiftIso Q n)) L)
                (Iso.app (Iso.symm (quotientCompQhIso C))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))) :
          (a : Q.obj K ⟶ (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n).obj L) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
                ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))
        (Function.comp (β := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
          (⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) :
            (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
              ShiftedHom (Q.obj K) (Q.obj L) n)
          toSmallShiftedHom)
        x :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))
    ((CategoryTheory.Functor.map Qh ∘
          (⇑toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)))
        x :
      Quiver.Hom (V := DerivedCategory C)
        (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
        (Functor.obj Qh
          (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))))

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_surjective, rfl