C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ { a := f.a ≫ h, b := fun i => b f i ≫ h }.a +
      ∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ b { a := f.a ≫ h, b := fun i => b f i ≫ h } (↑Fin.rev i) =
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a +
        ∑ i : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ b f (↑Fin.rev i)) ≫
      h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ φ (postComp f h) = φ f ≫ h
unfold φ postComp
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ { a := f.a ≫ h, b := fun i => b f i ≫ h }.a +
      ∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ b { a := f.a ≫ h, b := fun i => b f i ≫ h } (↑Fin.rev i) =
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a +
        ∑ i : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ b f (↑Fin.rev i)) ≫
      h
simp only [add_comp, sum_comp, assoc]