-- 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
h :
  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))) →
    Eq (α :=
      CohomologyClass K L n →
        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) :
        CohomologyClass K L n →
          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)) :
        CohomologyClass K L n →
          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))))
⊢ Function.Bijective (α := CohomologyClass K L n) (β :=
    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))

Tactic:
convert! (CochainComplex.IsKProjective.Qh_map_bijective _ _).comp (toHom_bijective K L n)

Premises used: CochainComplex.IsKProjective.Qh_map_bijective, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, Function.Bijective.comp