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