C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.hom.app K =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
change (N₁Γ₀.app K).hom = _
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
simp only [N₁Γ₀_app]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
rfl