C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f (P n) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f PInfty n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
rw [PInfty_f]
case zero
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.zero].op) ≫
      HomologicalComplex.Hom.f (P Nat.zero) Nat.zero =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.zero].op)

case succ
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.succ n].op) ≫
      HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.succ n].op)
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f (P n) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
rcases n with _|n
no goals
case zero
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.zero].op) ≫
      HomologicalComplex.Hom.f (P Nat.zero) Nat.zero =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.zero].op)
simpa only [P_f_0_eq] using comp_id _
no goals
case succ
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.succ n].op) ≫
      HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [Nat.succ n].op)
exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self