-- Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
theorem compatibility_Γ₂N₁_Γ₂N₂_natTrans (X : SimplicialObject C) :
    Γ₂N₁.natTrans.app X =
      (Γ₂N₂ToKaroubiIso.app X).inv ≫
        Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj { X := X, p := 𝟙 X, idem := ⋯ })) ≫
        (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Tactic:
erw [id_comp]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      (N₂ ⋙ Γ₂).map ((toKaroubi (SimplicialObject C)).obj X).decompId_i ≫
        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          ((toKaroubi (SimplicialObject C)).obj X).decompId_p

Tactic:
dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map,
  NatTrans.comp_app]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)

Tactic:
rw [Γ₂N₂.natTrans_app_f_app]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      (N₂ ⋙ Γ₂).map ((toKaroubi (SimplicialObject C)).obj X).decompId_i ≫
        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          ((toKaroubi (SimplicialObject C)).obj X).decompId_p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }

Tactic:
rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }

Tactic:
dsimp only [toKaroubi]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj { X := X, p := 𝟙 X, idem := ⋯ })) ≫
        (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Tactic:
rw [comp_id, Iso.inv_hom_id_app_assoc]

Result:
no goals