no goals
C : Type ?u.84246
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂ ⋙ Γ₂).obj P ⟶ (𝟭 (Karoubi (SimplicialObject C))).obj P
exact (N₂ ⋙ Γ₂).map P.decompId_i ≫
  (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p
C : Type u_1
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
              (toKaroubi (SimplicialObject C))).preimage
          (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans)).app
      P =
    (N₂ ⋙ Γ₂).map (Karoubi.decompId_i P) ≫ (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app P.X ≫ Karoubi.decompId_p P
C : Type u_1
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ natTrans.app P =
    (N₂ ⋙ Γ₂).map (Karoubi.decompId_i P) ≫ (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app P.X ≫ Karoubi.decompId_p P
dsimp only [natTrans]
no goals
C : Type u_1
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
              (toKaroubi (SimplicialObject C))).preimage
          (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans)).app
      P =
    (N₂ ⋙ Γ₂).map (Karoubi.decompId_i P) ≫ (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app P.X ≫ Karoubi.decompId_p P
rw [whiskeringLeft_obj_preimage_app
  (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans : _ ⟶ toKaroubi _ ⋙ 𝟭 _) P, Functor.id_map]