[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ∀ (i j : ℕ),
    ComplexShape.Rel (ComplexShape.down ℕ) i j →
      ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) i).hom ≫
          HomologicalComplex.d K i j =
        HomologicalComplex.d (Splitting.nondegComplex (Γ₀.splitting K)) i j ≫
          ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) j).hom
[PROOFSTEP]
rintro _ n (rfl : n + 1 = _)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) (n + 1)).hom ≫
      HomologicalComplex.d K (n + 1) n =
    HomologicalComplex.d (Splitting.nondegComplex (Γ₀.splitting K)) (n + 1) n ≫
      ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) n).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ 𝟙 (Splitting.N (Γ₀.splitting K) (n + 1)) ≫ HomologicalComplex.d K (n + 1) n =
    (Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj (Γ₀.obj K)) (n + 1) n ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))) ≫
      𝟙 (Splitting.N (Γ₀.splitting K) n)
[PROOFSTEP]
simp only [id_comp, comp_id, AlternatingFaceMapComplex.obj_d_eq, Preadditive.sum_comp, Preadditive.comp_sum]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.d K (n + 1) n =
    Finset.sum Finset.univ fun j =>
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
        ((-1) ^ ↑j • δ (Γ₀.obj K) j) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rw [Fintype.sum_eq_single (0 : Fin (n + 2))]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.d K (n + 1) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      ((-1) ^ ↑0 • δ (Γ₀.obj K) 0) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
simp only [Fin.val_zero, pow_zero, one_zsmul]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.d K (n + 1) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      δ (Γ₀.obj K) 0 ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
erw [Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_δ₀, Splitting.ι_πSummand_eq_id, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ∀ (x : Fin (n + 2)),
    x ≠ 0 →
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
          ((-1) ^ ↑x • δ (Γ₀.obj K) x) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
        0
[PROOFSTEP]
intro i hi
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      ((-1) ^ ↑i • δ (Γ₀.obj K) i) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
    0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      ((-1) ^ ↑i • δ (Γ₀.obj K) i) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
    0
[PROOFSTEP]
simp only [Preadditive.zsmul_comp, Preadditive.comp_zsmul, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (-1) ^ ↑i •
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
        δ (Γ₀.obj K) i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
    0
[PROOFSTEP]
erw [Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_eq_zero, zero_comp, zsmul_zero]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ [n + 1] ≠ [n]
[PROOFSTEP]
intro h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : [n + 1] = [n]
⊢ False
[PROOFSTEP]
replace h := congr_arg SimplexCategory.len h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : SimplexCategory.len [n + 1] = SimplexCategory.len [n]
⊢ False
[PROOFSTEP]
change n + 1 = n at h 
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : n + 1 = n
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case h₂
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)
[PROOFSTEP]
simpa only [Isδ₀.iff] using hi
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.app K =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
      (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
dsimp [N₁Γ₀]
[GOAL]
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (((Karoubi.Hom.mk PInfty ≫ NatTrans.app Split.toKaroubiNondegComplexFunctorIsoN₁.inv (Split.mk' (Γ₀.splitting K))) ≫
          Karoubi.Hom.mk (𝟙 (Splitting.nondegComplex (Γ₀.splitting K)))) ≫
        (toKaroubi (ChainComplex C ℕ)).map (NatTrans.app Γ₀'CompNondegComplexFunctor.hom K)) ≫
      Karoubi.Hom.mk (𝟙 K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
erw [id_comp, comp_id, comp_id]
[GOAL]
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app Split.toKaroubiNondegComplexFunctorIsoN₁.inv (Split.mk' (Γ₀.splitting K)) ≫
      (toKaroubi (ChainComplex C ℕ)).map (NatTrans.app Γ₀'CompNondegComplexFunctor.hom K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app N₁Γ₀.hom K =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
change (N₁Γ₀.app K).hom = _
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
simp only [N₁Γ₀_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app N₁Γ₀.inv K =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
      (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom
[PROOFSTEP]
change (N₁Γ₀.app K).inv = _
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
      (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom
[PROOFSTEP]
simp only [N₁Γ₀_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
      (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₁Γ₀.hom K).f n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv.f n
[PROOFSTEP]
rw [N₁Γ₀_hom_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₁Γ₀.inv K).f n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom.f n
[PROOFSTEP]
rw [N₁Γ₀_inv_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
apply id_comp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
[PROOFSTEP]
have h := Functor.congr_obj (functorExtension₂_comp_whiskeringLeft_toKaroubi (ChainComplex C ℕ) (SimplicialObject C)) Γ₀
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
h :
  (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C) ⋙
          (whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (SimplicialObject C))).obj
            (toKaroubi (ChainComplex C ℕ))).obj
      Γ₀ =
    ((whiskeringRight (ChainComplex C ℕ) (SimplicialObject C) (Karoubi (SimplicialObject C))).obj
          (toKaroubi (SimplicialObject C))).obj
      Γ₀
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
[PROOFSTEP]
have h' :=
  Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi (SimplicialObject C) (ChainComplex C ℕ)) N₁
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
h :
  (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C) ⋙
          (whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (SimplicialObject C))).obj
            (toKaroubi (ChainComplex C ℕ))).obj
      Γ₀ =
    ((whiskeringRight (ChainComplex C ℕ) (SimplicialObject C) (Karoubi (SimplicialObject C))).obj
          (toKaroubi (SimplicialObject C))).obj
      Γ₀
h' :
  (functorExtension₁ (SimplicialObject C) (ChainComplex C ℕ) ⋙
          (whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (ChainComplex C ℕ))).obj
            (toKaroubi (SimplicialObject C))).obj
      N₁ =
    (𝟭 (SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ))).obj N₁
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
[PROOFSTEP]
dsimp [N₂, Γ₂, functorExtension₁] at h h' ⊢
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
h :
  toKaroubi (ChainComplex C ℕ) ⋙ (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C)).obj Γ₀ =
    Γ₀ ⋙ toKaroubi (SimplicialObject C)
h' : toKaroubi (SimplicialObject C) ⋙ FunctorExtension₁.obj N₁ = N₁
⊢ toKaroubi (ChainComplex C ℕ) ⋙
      (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C)).obj Γ₀ ⋙ FunctorExtension₁.obj N₁ =
    Γ₀ ⋙ N₁
[PROOFSTEP]
rw [← Functor.assoc, h, Functor.assoc, h']
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv X).f n =
    HomologicalComplex.Hom.f X.p n ≫ Splitting.ιSummand (Γ₀.splitting X.X) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
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]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj (toKaroubi (ChainComplex C ℕ))).image_preimage e.hom
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
h :
  ((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
          (toKaroubi (ChainComplex C ℕ))).map
      (((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
            (toKaroubi (ChainComplex C ℕ))).preimage
        e.hom) =
    e.hom
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
h :
  whiskerLeft (toKaroubi (ChainComplex C ℕ))
      ((CategoryTheory.Functor.mk
            { obj := fun G => toKaroubi (ChainComplex C ℕ) ⋙ G,
              map := fun {X Y} α => whiskerLeft (toKaroubi (ChainComplex C ℕ)) α }).preimage
        (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom) =
    (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ))
      ((CategoryTheory.Functor.mk
            { obj := fun G => toKaroubi (ChainComplex C ℕ) ⋙ G,
              map := fun {X Y} α => whiskerLeft (toKaroubi (ChainComplex C ℕ)) α }).preimage
        (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom) =
    N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
exact h
