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 := g.app [n + 1].op ≫ f.a, b := fun i => g.app [n].op ≫ b f i }.a +
      ∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X' (Fin.succ (↑Fin.rev i)) ≫
            b { a := g.app [n + 1].op ≫ f.a, b := fun i => g.app [n].op ≫ b f i } (↑Fin.rev i) =
    g.app [n + 1].op ≫
      (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))
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'
⊢ φ (preComp f g) = g.app [n + 1].op ≫ φ f
unfold φ preComp
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 (P (n + 1)) (n + 1) ≫ g.app [n + 1].op ≫ f.a +
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X' (Fin.succ (↑Fin.rev x)) ≫ g.app [n].op ≫ b f (↑Fin.rev x) =
    g.app [n + 1].op ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a +
      g.app [n + 1].op ≫
        ∑ x : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b f (↑Fin.rev x)
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 := g.app [n + 1].op ≫ f.a, b := fun i => g.app [n].op ≫ b f i }.a +
      ∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X' (Fin.succ (↑Fin.rev i)) ≫
            b { a := g.app [n + 1].op ≫ f.a, b := fun i => g.app [n].op ≫ b f i } (↑Fin.rev i) =
    g.app [n + 1].op ≫
      (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))
simp only [PInfty_f, comp_add]
case e_a
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 (P (n + 1)) (n + 1) ≫ g.app [n + 1].op ≫ f.a =
    g.app [n + 1].op ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a

case e_a
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'
⊢ ∑ x : Fin (n + 1),
      HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
        SimplicialObject.δ X' (Fin.succ (↑Fin.rev x)) ≫ g.app [n].op ≫ b f (↑Fin.rev x) =
    g.app [n + 1].op ≫
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b f (↑Fin.rev x)
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 (P (n + 1)) (n + 1) ≫ g.app [n + 1].op ≫ f.a +
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X' (Fin.succ (↑Fin.rev x)) ≫ g.app [n].op ≫ b f (↑Fin.rev x) =
    g.app [n + 1].op ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a +
      g.app [n + 1].op ≫
        ∑ x : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b f (↑Fin.rev x)
congr 1
no goals
case e_a
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 (P (n + 1)) (n + 1) ≫ g.app [n + 1].op ≫ f.a =
    g.app [n + 1].op ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a
simp only [P_f_naturality_assoc]
no goals
case e_a
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'
⊢ ∑ x : Fin (n + 1),
      HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
        SimplicialObject.δ X' (Fin.succ (↑Fin.rev x)) ≫ g.app [n].op ≫ b f (↑Fin.rev x) =
    g.app [n + 1].op ≫
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b f (↑Fin.rev x)
simp only [comp_sum, P_f_naturality_assoc, SimplicialObject.δ_naturality_assoc]