no goals
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n = G.map (HomologicalComplex.Hom.f PInfty n)
simp only [PInfty_f, map_P]