∀ {R : Type u_2} [inst : Ring R] {C : Type u_3} [inst_1 : CategoryTheory.Category.{u_1, u_3} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] {X : C}
  (P : CategoryTheory.ProjectiveResolution X) (n : ℕ) (Y : C),
  (HomologicalComplex.sc (P.complex.linearYonedaObj R Y) n).HasHomology