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) ≫ (id X n).a +
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b (id X n) (↑Fin.rev x) =
    HomologicalComplex.Hom.f (P (n + 1)) (n + 1) + HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
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'
⊢ φ (id X n) = 𝟙 (X.obj [n + 1].op)
simp only [← P_add_Q_f (n + 1) (n + 1), φ]
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 PInfty (n + 1) ≫ (id X n).a = HomologicalComplex.Hom.f (P (n + 1)) (n + 1)

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)) ≫ b (id X n) (↑Fin.rev x) =
    HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
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) ≫ (id X n).a +
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b (id X n) (↑Fin.rev x) =
    HomologicalComplex.Hom.f (P (n + 1)) (n + 1) + HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
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'
⊢ ∑ x : Fin (n + 1),
      HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫ SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ b (id X n) (↑Fin.rev x) =
    HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
. exact Eq.trans (by congr ; simp) (decomposition_Q n (n + 1)).symm
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 PInfty (n + 1) ≫ (id X n).a = HomologicalComplex.Hom.f (P (n + 1)) (n + 1)
simp only [id, PInfty_f, P_f_idem]
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)) ≫ b (id X n) (↑Fin.rev x) =
    HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
exact Eq.trans (by congr ; simp) (decomposition_Q n (n + 1)).symm
case e_s
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'
⊢ Finset.univ = Finset.filter (fun i => ↑i < n + 1) Finset.univ
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)) ≫ b (id X n) (↑Fin.rev x) =
    ∑ i in Finset.filter (fun i => ↑i < n + 1) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)
congr
no goals
case e_s
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'
⊢ Finset.univ = Finset.filter (fun i => ↑i < n + 1) Finset.univ
simp