C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
      (N₂ ⋙ Γ₂).map (Karoubi.decompId_i ((toKaroubi (SimplicialObject C)).obj X)) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          Karoubi.decompId_p ((toKaroubi (SimplicialObject C)).obj X)
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X = (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)
rw [Γ₂N₂.natTrans_app_f_app]
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙 (Karoubi.mk ((toKaroubi (SimplicialObject C)).obj X).X (𝟙 ((toKaroubi (SimplicialObject C)).obj X).X))
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
      (N₂ ⋙ Γ₂).map (Karoubi.decompId_i ((toKaroubi (SimplicialObject C)).obj X)) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          Karoubi.decompId_p ((toKaroubi (SimplicialObject C)).obj X)
dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map,
  NatTrans.comp_app]
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    compatibility_Γ₂N₁_Γ₂N₂.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙 (Karoubi.mk ((toKaroubi (SimplicialObject C)).obj X).X (𝟙 ((toKaroubi (SimplicialObject C)).obj X).X))
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙 (Karoubi.mk ((toKaroubi (SimplicialObject C)).obj X).X (𝟙 ((toKaroubi (SimplicialObject C)).obj X).X))
rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    compatibility_Γ₂N₁_Γ₂N₂.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj (Karoubi.mk X (𝟙 X)))) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 (Karoubi.mk X (𝟙 X))
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    compatibility_Γ₂N₁_Γ₂N₂.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙 (Karoubi.mk ((toKaroubi (SimplicialObject C)).obj X).X (𝟙 ((toKaroubi (SimplicialObject C)).obj X).X))
dsimp only [toKaroubi]
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    compatibility_Γ₂N₁_Γ₂N₂.inv.app X ≫
      (compatibility_Γ₂N₁_Γ₂N₂.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 (Karoubi.mk X (𝟙 X))
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    compatibility_Γ₂N₁_Γ₂N₂.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj (Karoubi.mk X (𝟙 X)))) ≫
        (compatibility_Γ₂N₁_Γ₂N₂.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 (Karoubi.mk X (𝟙 X))
erw [id_comp]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    compatibility_Γ₂N₁_Γ₂N₂.inv.app X ≫
      (compatibility_Γ₂N₁_Γ₂N₂.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 (Karoubi.mk X (𝟙 X))
rw [comp_id, Iso.inv_hom_id_app_assoc]