no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ (homotopyEquiv P Q).inv ≫ P.π = Q.π
simp [homotopyEquiv]