C : Type u_1
inst✝² : Category 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₁
C : Type u_1
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
have h := Functor.congr_obj (functorExtension₂_comp_whiskeringLeft_toKaroubi
  (ChainComplex C ℕ) (SimplicialObject C)) Γ₀
C : Type u_1
inst✝² : Category 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₁
C : Type u_1
inst✝² : Category 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₁
have h' := Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi
  (SimplicialObject C) (ChainComplex C ℕ)) N₁
C : Type u_1
inst✝² : Category 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₁
C : Type u_1
inst✝² : Category 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₁
dsimp [N₂, Γ₂, functorExtension₁] at h h' ⊢
no goals
C : Type u_1
inst✝² : Category 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₁
rw [← Functor.assoc, h, Functor.assoc, h']