-- Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean
theorem compatibility_N₂_N₁_karoubi :
    N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor =
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        N₁ ⋙ (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
            Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse _

Proof state:
case refine_1.refine_1.h.h_X
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X n).X =
    (((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                N₁ ⋙
                  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                    (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
            P).X
        n).X

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
                P).d
            i j

Tactic:
rintro _ n (rfl : n + 1 = _)

Result:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d (n + 1) n ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫
      ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                N₁ ⋙
                  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                    (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
            P).d
        (n + 1) n

Proof state:
case refine_1.refine_2.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d (n + 1) n ≫ eqToHom ⋯).f =
    (eqToHom ⋯ ≫
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).d
          (n + 1) n).f

Tactic:
have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n

Result:
case refine_1.refine_2.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
h :
  (AlternatingFaceMapComplex.map P.p).f (n + 1) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n =
    (AlternatingFaceMapComplex.obj P.X).d (n + 1) n ≫ (AlternatingFaceMapComplex.map P.p).f n
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d (n + 1) n ≫ eqToHom ⋯).f =
    (eqToHom ⋯ ≫
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).d
          (n + 1) n).f

Proof state:
case refine_2.h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P Q : Karoubi (SimplicialObject C)
f : P ⟶ Q
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f).f n).f =
    ((eqToHom ⋯ ≫
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).map
                f ≫
              eqToHom ⋯).f
        n).f

Tactic:
dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]

Result:
case refine_2.h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P Q : Karoubi (SimplicialObject C)
f : P ⟶ Q
n : ℕ
⊢ PInfty.f n ≫ f.f.app (op ⦋n⦌) = ((eqToHom ⋯).f n).f ≫ ((PInfty.f n).f ≫ f.f.app (op ⦋n⦌)) ≫ ((eqToHom ⋯).f n).f

Proof state:
case refine_1.refine_2.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
h :
  P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n =
    (AlternatingFaceMapComplex.obj P.X).d (n + 1) n ≫ P.p.app (op ⦋n⦌)
⊢ ((PInfty.f (n + 1) ≫ P.p.app (op ⦋n + 1⦌)) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n) ≫ (eqToHom ⋯).f =
    (eqToHom ⋯).f ≫
      (PInfty.f (n + 1)).f ≫ ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f

Tactic:
simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id,
  karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f,
  ← HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]

Result:
no goals

Proof state:
case refine_1.refine_2.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
h :
  (AlternatingFaceMapComplex.map P.p).f (n + 1) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n =
    (AlternatingFaceMapComplex.obj P.X).d (n + 1) n ≫ (AlternatingFaceMapComplex.map P.p).f n
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d (n + 1) n ≫ eqToHom ⋯).f =
    (eqToHom ⋯ ≫
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).d
          (n + 1) n).f

Tactic:
dsimp [N₂, karoubiChainComplexEquivalence,
  KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢

Result:
case refine_1.refine_2.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
h :
  P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n =
    (AlternatingFaceMapComplex.obj P.X).d (n + 1) n ≫ P.p.app (op ⦋n⦌)
⊢ ((PInfty.f (n + 1) ≫ P.p.app (op ⦋n + 1⦌)) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n) ≫ (eqToHom ⋯).f =
    (eqToHom ⋯).f ≫
      (PInfty.f (n + 1)).f ≫ ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor =
    karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
      N₁ ⋙
        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
          (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)

Tactic:
refine CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_

Result:
case refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P =
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          N₁ ⋙
            (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
              (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
      P

case refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P Q : Karoubi (SimplicialObject C)
f : P ⟶ Q
⊢ (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f =
    eqToHom ⋯ ≫
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              N₁ ⋙
                (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).map
          f ≫
        eqToHom ⋯