C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f
      ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
          (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f
      n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv.f n
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f (N₁Γ₀.hom.app K).f n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv.f n
rw [N₁Γ₀_hom_app]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f
      ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
          (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f
      n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv.f n
apply comp_id