case w
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.app K =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
      (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)
ext1
case w
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (((Karoubi.Hom.mk PInfty ≫ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K))) ≫
          Karoubi.Hom.mk (𝟙 (Splitting.nondegComplex (Γ₀.splitting K)))) ≫
        (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K)) ≫
      Karoubi.Hom.mk (𝟙 K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
case w
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom
dsimp [N₁Γ₀]
case w
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K)) ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
case w
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (((Karoubi.Hom.mk PInfty ≫ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K))) ≫
          Karoubi.Hom.mk (𝟙 (Splitting.nondegComplex (Γ₀.splitting K)))) ≫
        (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K)) ≫
      Karoubi.Hom.mk (𝟙 K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
erw [id_comp, comp_id, comp_id]
no goals
case w
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K)) ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
rfl