no goals
C : Type u_1
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ HomologicalComplex.Hom.f (N₂Γ₂.inv.app X).f n =
    HomologicalComplex.Hom.f X.p n ≫ Splitting.ιSummand (Γ₀.splitting X.X) (Splitting.IndexSet.id [n].op)
simp only [N₂Γ₂, Functor.preimageIso, Iso.trans,
  whiskeringLeft_obj_preimage_app, N₂Γ₂ToKaroubiIso_inv, assoc,
  Functor.id_map, NatTrans.comp_app, eqToHom_app, Karoubi.comp_f,
  Karoubi.eqToHom_f, Karoubi.decompId_p_f, HomologicalComplex.comp_f,
  N₁Γ₀_inv_app_f_f, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
  Functor.comp_map, Functor.comp_obj, Karoubi.decompId_i_f,
  eqToHom_refl, comp_id, N₂_map_f_f, Γ₂_map_f_app, N₁_obj_p,
  PInfty_on_Γ₀_splitting_summand_eq_self_assoc, toKaroubi_obj_X,
  Splitting.ι_desc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk, unop_op,
  Karoubi.HomologicalComplex.p_idem_assoc]