-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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
⊢ 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))))
have 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))))
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x