no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ HomologicalComplex.Hom.f (Q (q + 1)) n = HomologicalComplex.Hom.f (Q q) n
simp only [Q, HomologicalComplex.sub_f_apply, P_is_eventually_constant hqn]