[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.τ₀ =
    Compatibility.τ₁
      (eqToIso (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
      (eqToIso
        (_ :
          (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
            Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
      N₁Γ₀
[PROOFSTEP]
ext K : 3
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app Compatibility.τ₀.hom K =
    NatTrans.app
      (Compatibility.τ₁
          (eqToIso
            (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
          (eqToIso
            (_ :
              (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
                Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
          N₁Γ₀).hom
      K
[PROOFSTEP]
simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app, eqToIso.hom]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app Preadditive.DoldKan.equivalence.counitIso.hom ((toKaroubiEquivalence (ChainComplex C ℕ)).functor.obj K) =
    Preadditive.DoldKan.equivalence.functor.map
        (NatTrans.app
          (eqToHom
            (_ :
              (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
                Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
          K) ≫
      NatTrans.app
          (eqToHom
            (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
          (Γ.obj K) ≫
        NatTrans.app N₁Γ₀.hom K
[PROOFSTEP]
refine' (N₂Γ₂_compatible_with_N₁Γ₀ K).trans _
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app N₂Γ₂ToKaroubiIso.hom K ≫ NatTrans.app N₁Γ₀.hom K =
    Preadditive.DoldKan.equivalence.functor.map
        (NatTrans.app
          (eqToHom
            (_ :
              (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
                Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
          K) ≫
      NatTrans.app
          (eqToHom
            (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
          (Γ.obj K) ≫
        NatTrans.app N₁Γ₀.hom K
[PROOFSTEP]
simp only [N₂Γ₂ToKaroubiIso_hom, eqToHom_map, eqToHom_app, eqToHom_trans_assoc]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ
      (eqToIso
        (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁)) =
    Γ₂N₁
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ (Compatibility.υ
        (eqToIso
          (_ :
            (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))).hom =
    Γ₂N₁.hom
[PROOFSTEP]
rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
[GOAL]
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Γ₂N₁.inv ≫
      (Compatibility.υ
          (eqToIso
            (_ :
              (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                N₁))).hom =
    𝟙 (N₁ ⋙ Γ₂)
[PROOFSTEP]
ext X : 2
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app
      (Γ₂N₁.inv ≫
        (Compatibility.υ
            (eqToIso
              (_ :
                (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                  N₁))).hom)
      X =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.inv X ≫
      NatTrans.app
        (Compatibility.υ
            (eqToIso
              (_ :
                (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                  N₁))).hom
        X =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
erw [compatibility_Γ₂N₁_Γ₂N₂_natTrans X]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫ NatTrans.app Γ₂N₂.natTrans ((toKaroubi (SimplicialObject C)).obj X)) ≫
      NatTrans.app
        (Compatibility.υ
            (eqToIso
              (_ :
                (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                  N₁))).hom
        X =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
rw [Compatibility.υ_hom_app, Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      NatTrans.app Γ₂N₂.natTrans ((toKaroubi (SimplicialObject C)).obj X) ≫
        NatTrans.app Γ₂N₂.hom ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
          Preadditive.DoldKan.equivalence.inverse.map
            (NatTrans.app
              (eqToIso
                  (_ :
                    (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                      N₁)).hom
              X) =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
erw [← NatTrans.comp_app_assoc, IsIso.hom_inv_id]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      NatTrans.app (𝟙 (N₂ ⋙ Γ₂)) ((toKaroubi (SimplicialObject C)).obj X) ≫
        Preadditive.DoldKan.equivalence.inverse.map
          (NatTrans.app
            (eqToIso
                (_ :
                  (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                    N₁)).hom
            X) =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
rw [NatTrans.id_app, id_comp, NatTrans.id_app, eqToIso.hom, eqToHom_app, eqToHom_map]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      eqToHom
        (_ :
          Preadditive.DoldKan.equivalence.inverse.obj
              (Preadditive.DoldKan.equivalence.functor.obj
                ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X)) =
            Preadditive.DoldKan.equivalence.inverse.obj (N₁.obj X)) =
    𝟙 ((N₁ ⋙ Γ₂).obj X)
[PROOFSTEP]
rw [compatibility_Γ₂N₁_Γ₂N₂_inv_app, eqToHom_trans, eqToHom_refl]
