[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) n = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
rcases n with (_ | n)
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hqn : Nat.zero ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) Nat.zero = HomologicalComplex.Hom.f (P q) Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, P_f_0_eq]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : Nat.succ n ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) (Nat.succ n) = HomologicalComplex.Hom.f (P q) (Nat.succ n)
[PROOFSTEP]
simp only [P_succ, add_right_eq_self, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : Nat.succ n ≤ q
⊢ HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ HomologicalComplex.Hom.f (Hσ q) (Nat.succ n) = 0
[PROOFSTEP]
exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ HomologicalComplex.Hom.f (Q (q + 1)) n = HomologicalComplex.Hom.f (Q q) n
[PROOFSTEP]
simp only [Q, HomologicalComplex.sub_f_apply, P_is_eventually_constant hqn]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.41303, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (fun n => HomologicalComplex.Hom.f (P n) n) (n + 1) ≫ AlternatingFaceMapComplex.objD X n =
    AlternatingFaceMapComplex.objD X n ≫ (fun n => HomologicalComplex.Hom.f (P n) n) n
[PROOFSTEP]
simpa only [← P_is_eventually_constant (show n ≤ n by rfl), AlternatingFaceMapComplex.obj_d_eq] using
  (P (n + 1) : K[X] ⟶ _).comm (n + 1) n
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.41303, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f QInfty 0 = 0
[PROOFSTEP]
dsimp [QInfty]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (X.obj (op [0])) - 𝟙 (X.obj (op [0])) = 0
[PROOFSTEP]
simp only [sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
simp only [PInfty_f, P_f_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ PInfty = PInfty
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (PInfty ≫ PInfty) n = HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
exact PInfty_f_idem n
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ QInfty = QInfty
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (QInfty ≫ QInfty) n = HomologicalComplex.Hom.f QInfty n
[PROOFSTEP]
exact QInfty_f_idem n
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f QInfty n = 0
[PROOFSTEP]
dsimp only [QInfty]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (𝟙 K[X] - PInfty) n = 0
[PROOFSTEP]
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, comp_id, PInfty_f_idem, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ QInfty = 0
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (PInfty ≫ QInfty) n = HomologicalComplex.Hom.f 0 n
[PROOFSTEP]
apply PInfty_f_comp_QInfty_f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f QInfty n ≫ HomologicalComplex.Hom.f PInfty n = 0
[PROOFSTEP]
dsimp only [QInfty]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (𝟙 K[X] - PInfty) n ≫ HomologicalComplex.Hom.f PInfty n = 0
[PROOFSTEP]
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, sub_comp, id_comp, PInfty_f_idem, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ PInfty = 0
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (QInfty ≫ PInfty) n = HomologicalComplex.Hom.f 0 n
[PROOFSTEP]
apply QInfty_f_comp_PInfty_f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + QInfty = 𝟙 K[X]
[PROOFSTEP]
dsimp only [QInfty]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]
[PROOFSTEP]
simp only [add_sub_cancel'_right]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.354986, u_1} C
inst✝ : Preadditive C
X✝ X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C).map f ≫ (fun x => PInfty) Y = (fun x => PInfty) X ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.354986, u_1} C
inst✝ : Preadditive C
X✝ X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f ≫ (fun x => PInfty) Y) n =
    HomologicalComplex.Hom.f ((fun x => PInfty) X ≫ (alternatingFaceMapComplex C).map f) n
[PROOFSTEP]
exact PInfty_f_naturality n f
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n = G.map (HomologicalComplex.Hom.f PInfty n)
[PROOFSTEP]
simp only [PInfty_f, map_P]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let Y₁ := (karoubiFunctorCategoryEmbedding _ _).obj Y
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let Y₂ := Y.X
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let Y₃ := ((whiskering _ _).obj (toKaroubi C)).obj Y.X
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let Y₄ := (karoubiFunctorCategoryEmbedding _ _).obj ((toKaroubi _).obj Y.X)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let P₁ : K[Y₁] ⟶ _ := PInfty
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let P₂ : K[Y₂] ⟶ _ := PInfty
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let P₃ : K[Y₃] ⟶ _ := PInfty
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
let P₄ : K[Y₄] ⟶ _ := PInfty
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
⊢ (HomologicalComplex.Hom.f PInfty n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
change (P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
⊢ (HomologicalComplex.Hom.f P₁ n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f P₂ n
[PROOFSTEP]
have h₃₂ : (P₃.f n).f = P₂.f n := Karoubi.hom_ext_iff.mp (map_PInfty_f (toKaroubi C) Y₂ n)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
⊢ (HomologicalComplex.Hom.f P₁ n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f P₂ n
[PROOFSTEP]
have h₄₃ : P₄.f n = P₃.f n :=
  by
  have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
  simp only [← natTransPInfty_f_app]
  congr 1
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
⊢ HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
[PROOFSTEP]
have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h :
  (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y₂ =
    ((whiskeringRight SimplexCategoryᵒᵖ C (Karoubi C)).obj (toKaroubi C)).obj Y₂
⊢ HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
[PROOFSTEP]
simp only [← natTransPInfty_f_app]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h :
  (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y₂ =
    ((whiskeringRight SimplexCategoryᵒᵖ C (Karoubi C)).obj (toKaroubi C)).obj Y₂
⊢ NatTrans.app (natTransPInfty_f (Karoubi C) n)
      ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)) =
    NatTrans.app (natTransPInfty_f (Karoubi C) n) (((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X)
[PROOFSTEP]
congr 1
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
⊢ (HomologicalComplex.Hom.f P₁ n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f P₂ n
[PROOFSTEP]
have h₁₄ :=
  Idempotents.natTrans_eq ((𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)) ◫ (natTransPInfty_f (Karoubi C) n))
    Y
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  NatTrans.app (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n) Y =
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map
        (Karoubi.decompId_i Y) ≫
      NatTrans.app (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n)
          (Karoubi.mk Y.X (𝟙 Y.X)) ≫
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map
          (Karoubi.decompId_p Y)
⊢ (HomologicalComplex.Hom.f P₁ n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f P₂ n
[PROOFSTEP]
dsimp [natTransPInfty_f] at h₁₄ 
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  (Karoubi.Hom.mk (NatTrans.app Y.p (op [n])) ≫ HomologicalComplex.Hom.f PInfty n) ≫
      Karoubi.Hom.mk (NatTrans.app Y.p (op [n])) =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      ((Karoubi.Hom.mk (𝟙 (Y.X.obj (op [n]))) ≫ HomologicalComplex.Hom.f PInfty n) ≫
          Karoubi.Hom.mk (𝟙 (Y.X.obj (op [n])))) ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
⊢ (HomologicalComplex.Hom.f P₁ n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f P₂ n
[PROOFSTEP]
erw [id_comp, id_comp, comp_id, comp_id] at h₁₄ 
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
⊢ (HomologicalComplex.Hom.f P₁ n).f = NatTrans.app Y.p (op [n]) ≫ HomologicalComplex.Hom.f P₂ n
[PROOFSTEP]
rw [← h₃₂, ← h₄₃, h₁₄]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
⊢ (NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
        HomologicalComplex.Hom.f PInfty n ≫
          NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])).f =
    NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f P₄ n).f
[PROOFSTEP]
simp only [KaroubiFunctorCategoryEmbedding.map_app_f, Karoubi.decompId_p_f, Karoubi.decompId_i_f, Karoubi.comp_f]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
⊢ NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app Y.p (op [n]) =
    NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f
[PROOFSTEP]
let π : Y₄ ⟶ Y₄ := (toKaroubi _ ⋙ karoubiFunctorCategoryEmbedding _ _).map Y.p
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
⊢ NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app Y.p (op [n]) =
    NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f
[PROOFSTEP]
have eq := Karoubi.hom_ext_iff.mp (PInfty_f_naturality n π)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq :
  (NatTrans.app π (op [n]) ≫ HomologicalComplex.Hom.f PInfty n).f =
    (HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app π (op [n])).f
⊢ NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app Y.p (op [n]) =
    NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f
[PROOFSTEP]
simp only [Karoubi.comp_f] at eq 
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq :
  (NatTrans.app ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p)
          (op [n])).f ≫
      (HomologicalComplex.Hom.f PInfty n).f =
    (HomologicalComplex.Hom.f PInfty n).f ≫
      (NatTrans.app ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p)
          (op [n])).f
⊢ NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app Y.p (op [n]) =
    NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f
[PROOFSTEP]
dsimp at eq 
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (HomologicalComplex.Hom.f P₃ n).f = HomologicalComplex.Hom.f P₂ n
h₄₃ : HomologicalComplex.Hom.f P₄ n = HomologicalComplex.Hom.f P₃ n
h₁₄ :
  HomologicalComplex.Hom.f PInfty n =
    NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_i Y)) (op [n]) ≫
      HomologicalComplex.Hom.f PInfty n ≫
        NatTrans.app (KaroubiFunctorCategoryEmbedding.map (Karoubi.decompId_p Y)) (op [n])
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq :
  NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f =
    (HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app Y.p (op [n])
⊢ NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app Y.p (op [n]) =
    NatTrans.app Y.p (op [n]) ≫ (HomologicalComplex.Hom.f PInfty n).f
[PROOFSTEP]
rw [← eq, app_idem_assoc Y (op [n])]
