[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])]


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.28, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ∀ [inst : IsIso (N₁.map f)], IsIso f
[PROOFSTEP]
intro
  -- restating the result in a way that allows induction on the degree n
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
⊢ IsIso f
[PROOFSTEP]
suffices ∀ n : ℕ, IsIso (f.app (op [n]))
  by
  haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
  apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
this : ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
⊢ IsIso f
[PROOFSTEP]
haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
this✝ : ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
this : ∀ (Δ : SimplexCategoryᵒᵖ), IsIso (NatTrans.app f Δ)
⊢ IsIso f
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
⊢ ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
[PROOFSTEP]
have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), HomologicalComplex.Hom.f (N₁.map f ≫ inv (N₁.map f)).f i = HomologicalComplex.Hom.f (𝟙 (N₁.obj X)).f i
⊢ ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
[PROOFSTEP]
have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), HomologicalComplex.Hom.f (N₁.map f ≫ inv (N₁.map f)).f i = HomologicalComplex.Hom.f (𝟙 (N₁.obj X)).f i
h₂ : ∀ (i : ℕ), HomologicalComplex.Hom.f (inv (N₁.map f) ≫ N₁.map f).f i = HomologicalComplex.Hom.f (𝟙 (N₁.obj Y)).f i
⊢ ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
[PROOFSTEP]
have h₃ := fun n => Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op [n]))
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₁ : ∀ (i : ℕ), HomologicalComplex.Hom.f (N₁.map f ≫ inv (N₁.map f)).f i = HomologicalComplex.Hom.f (𝟙 (N₁.obj X)).f i
h₂ : ∀ (i : ℕ), HomologicalComplex.Hom.f (inv (N₁.map f) ≫ N₁.map f).f i = HomologicalComplex.Hom.f (𝟙 (N₁.obj Y)).f i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f (N₁.obj Y).p n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f (N₁.obj X).p n ≫ NatTrans.app f (op [n])
⊢ ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
[PROOFSTEP]
simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f, AlternatingFaceMapComplex.map_f, N₁_obj_p,
  Karoubi.id_eq, assoc] at h₁ h₂ h₃
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
⊢ ∀ (n : ℕ), IsIso (NatTrans.app f (op [n]))
[PROOFSTEP]
intro n
[GOAL]
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
n : ℕ
⊢ IsIso (NatTrans.app f (op [n]))
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
⊢ IsIso (NatTrans.app f (op [Nat.zero]))
[PROOFSTEP]
use(inv (N₁.map f)).f.f 0
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
⊢ NatTrans.app f (op [Nat.zero]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [Nat.zero])) ∧
    HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ NatTrans.app f (op [Nat.zero]) = 𝟙 (Y.obj (op [Nat.zero]))
[PROOFSTEP]
have h₁₀ := h₁ 0
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
h₁₀ :
  HomologicalComplex.Hom.f PInfty 0 ≫ NatTrans.app f (op [0]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 =
    HomologicalComplex.Hom.f PInfty 0
⊢ NatTrans.app f (op [Nat.zero]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [Nat.zero])) ∧
    HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ NatTrans.app f (op [Nat.zero]) = 𝟙 (Y.obj (op [Nat.zero]))
[PROOFSTEP]
have h₂₀ := h₂ 0
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
h₁₀ :
  HomologicalComplex.Hom.f PInfty 0 ≫ NatTrans.app f (op [0]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 =
    HomologicalComplex.Hom.f PInfty 0
h₂₀ :
  HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ HomologicalComplex.Hom.f PInfty 0 ≫ NatTrans.app f (op [0]) =
    HomologicalComplex.Hom.f PInfty 0
⊢ NatTrans.app f (op [Nat.zero]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [Nat.zero])) ∧
    HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ NatTrans.app f (op [Nat.zero]) = 𝟙 (Y.obj (op [Nat.zero]))
[PROOFSTEP]
dsimp at h₁₀ h₂₀
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
h₁₀ : 𝟙 (X.obj (op [0])) ≫ NatTrans.app f (op [0]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [0]))
h₂₀ : HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ 𝟙 (X.obj (op [0])) ≫ NatTrans.app f (op [0]) = 𝟙 (Y.obj (op [0]))
⊢ NatTrans.app f (op [Nat.zero]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [Nat.zero])) ∧
    HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ NatTrans.app f (op [Nat.zero]) = 𝟙 (Y.obj (op [Nat.zero]))
[PROOFSTEP]
simp only [id_comp, comp_id] at h₁₀ h₂₀
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
h₁₀ : NatTrans.app f (op [0]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [0]))
h₂₀ : HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ NatTrans.app f (op [0]) = 𝟙 (Y.obj (op [0]))
⊢ NatTrans.app f (op [Nat.zero]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 = 𝟙 (X.obj (op [Nat.zero])) ∧
    HomologicalComplex.Hom.f (inv (N₁.map f)).f 0 ≫ NatTrans.app f (op [Nat.zero]) = 𝟙 (Y.obj (op [Nat.zero]))
[PROOFSTEP]
tauto
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
n : ℕ
hn : IsIso (NatTrans.app f (op [n]))
⊢ IsIso (NatTrans.app f (op [Nat.succ n]))
[PROOFSTEP]
haveI := hn
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
n : ℕ
hn this : IsIso (NatTrans.app f (op [n]))
⊢ IsIso (NatTrans.app f (op [Nat.succ n]))
[PROOFSTEP]
use φ {
      a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
      b := fun i => inv (f.app (op [n])) ≫ X.σ i }
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.28, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f (inv (N₁.map f)).f i ≫ HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) =
      HomologicalComplex.Hom.f PInfty i
h₃ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ NatTrans.app f (op [n]) =
      HomologicalComplex.Hom.f (inv (N₁.map f)).f n ≫ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f (op [n])
h₁ :
  ∀ (i : ℕ),
    HomologicalComplex.Hom.f PInfty i ≫ NatTrans.app f (op [i]) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f i =
      HomologicalComplex.Hom.f PInfty i
n : ℕ
hn this : IsIso (NatTrans.app f (op [n]))
⊢ NatTrans.app f (op [Nat.succ n]) ≫
        φ
          { a := HomologicalComplex.Hom.f PInfty (n + 1) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f (n + 1),
            b := fun i => inv (NatTrans.app f (op [n])) ≫ SimplicialObject.σ X i } =
      𝟙 (X.obj (op [Nat.succ n])) ∧
    φ
          { a := HomologicalComplex.Hom.f PInfty (n + 1) ≫ HomologicalComplex.Hom.f (inv (N₁.map f)).f (n + 1),
            b := fun i => inv (NatTrans.app f (op [n])) ≫ SimplicialObject.σ X i } ≫
        NatTrans.app f (op [Nat.succ n]) =
      𝟙 (Y.obj (op [Nat.succ n]))
[PROOFSTEP]
simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp, PInfty_f_naturality_assoc,
  IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc, SimplicialObject.σ_naturality, h₁, h₂, h₃]
[GOAL]
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 ⋙
          Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
[PROOFSTEP]
refine' CategoryTheory.Functor.ext (fun P => _) fun P Q f => _
[GOAL]
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 ⋙
              Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
      P
[PROOFSTEP]
refine' HomologicalComplex.ext _ _
[GOAL]
case refine'_1.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).X =
    ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            N₁ ⋙
              (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
        P).X
[PROOFSTEP]
ext n
[GOAL]
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 : ℕ
⊢ (HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n).X =
    (HomologicalComplex.X
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              N₁ ⋙
                (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
          P)
        n).X
[PROOFSTEP]
rfl
[GOAL]
case refine'_1.refine'_1.h.h_p
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n).p ≫
      eqToHom
        (_ :
          (HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n).X =
            (HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n).X) =
    eqToHom
        (_ :
          (HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n).X =
            (HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n).X) ≫
      (HomologicalComplex.X
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                N₁ ⋙
                  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                    Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
            P)
          n).p
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1.refine'_1.h.h_p
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])) ≫ 𝟙 (P.X.obj (op [n])) =
    𝟙 (P.X.obj (op [n])) ≫ (HomologicalComplex.Hom.f PInfty n).f
[PROOFSTEP]
simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp, eqToHom_refl]
[GOAL]
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.Rel (ComplexShape.down ℕ) i j →
      HomologicalComplex.d ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) i j ≫
          eqToHom
            (_ :
              HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) j =
                HomologicalComplex.X
                  ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                        N₁ ⋙
                          (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                            Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                              (ComplexShape.down ℕ)).obj
                    P)
                  j) =
        eqToHom
            (_ :
              HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) i =
                HomologicalComplex.X
                  ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                        N₁ ⋙
                          (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                            Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                              (ComplexShape.down ℕ)).obj
                    P)
                  i) ≫
          HomologicalComplex.d
            ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
              P)
            i j
[PROOFSTEP]
rintro _ n (rfl : n + 1 = _)
[GOAL]
case refine'_1.refine'_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ HomologicalComplex.d ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) (n + 1) n ≫
      eqToHom
        (_ :
          HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n =
            HomologicalComplex.X
              ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
                P)
              n) =
    eqToHom
        (_ :
          HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) (n + 1) =
            HomologicalComplex.X
              ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
                P)
              (n + 1)) ≫
      HomologicalComplex.d
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              N₁ ⋙
                (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
          P)
        (n + 1) n
[PROOFSTEP]
ext
[GOAL]
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 : ℕ
⊢ (HomologicalComplex.d ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) (n + 1) n ≫
        eqToHom
          (_ :
            HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n =
              HomologicalComplex.X
                ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                      N₁ ⋙
                        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                          Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                            (ComplexShape.down ℕ)).obj
                  P)
                n)).f =
    (eqToHom
          (_ :
            HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) (n + 1) =
              HomologicalComplex.X
                ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                      N₁ ⋙
                        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                          Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                            (ComplexShape.down ℕ)).obj
                  P)
                (n + 1)) ≫
        HomologicalComplex.d
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                N₁ ⋙
                  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                    Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
            P)
          (n + 1) n).f
[PROOFSTEP]
have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
[GOAL]
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 :
  HomologicalComplex.Hom.f (AlternatingFaceMapComplex.map P.p) (n + 1) ≫
      HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n =
    HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n ≫
      HomologicalComplex.Hom.f (AlternatingFaceMapComplex.map P.p) n
⊢ (HomologicalComplex.d ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) (n + 1) n ≫
        eqToHom
          (_ :
            HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) n =
              HomologicalComplex.X
                ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                      N₁ ⋙
                        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                          Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                            (ComplexShape.down ℕ)).obj
                  P)
                n)).f =
    (eqToHom
          (_ :
            HomologicalComplex.X ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P) (n + 1) =
              HomologicalComplex.X
                ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                      N₁ ⋙
                        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                          Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                            (ComplexShape.down ℕ)).obj
                  P)
                (n + 1)) ≫
        HomologicalComplex.d
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                N₁ ⋙
                  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                    Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
            P)
          (n + 1) n).f
[PROOFSTEP]
dsimp [N₂, karoubiChainComplexEquivalence, KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢
[GOAL]
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 :
  NatTrans.app P.p (op [n + 1]) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n =
    HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n ≫ NatTrans.app P.p (op [n])
⊢ ((HomologicalComplex.Hom.f PInfty (n + 1) ≫ NatTrans.app P.p (op [n + 1])) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n) ≫
      (eqToHom
          (_ :
            Karoubi.mk (P.X.obj (op [n])) (HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])) =
              HomologicalComplex.X
                ((Functor.mapHomologicalComplex (KaroubiKaroubi.inverse C) (ComplexShape.down ℕ)).obj
                  (HomologicalComplex.mk
                    (fun n =>
                      Karoubi.mk ((KaroubiFunctorCategoryEmbedding.obj P).obj (op [n]))
                        (HomologicalComplex.Hom.f PInfty n))
                    fun i j =>
                    Karoubi.Hom.mk
                      (HomologicalComplex.Hom.f PInfty i ≫
                        HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) i
                          j)))
                n)).f =
    (eqToHom
          (_ :
            Karoubi.mk (P.X.obj (op [n + 1]))
                (HomologicalComplex.Hom.f PInfty (n + 1) ≫ NatTrans.app P.p (op [n + 1])) =
              HomologicalComplex.X
                ((Functor.mapHomologicalComplex (KaroubiKaroubi.inverse C) (ComplexShape.down ℕ)).obj
                  (HomologicalComplex.mk
                    (fun n =>
                      Karoubi.mk ((KaroubiFunctorCategoryEmbedding.obj P).obj (op [n]))
                        (HomologicalComplex.Hom.f PInfty n))
                    fun i j =>
                    Karoubi.Hom.mk
                      (HomologicalComplex.Hom.f PInfty i ≫
                        HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) i
                          j)))
                (n + 1))).f ≫
      (HomologicalComplex.Hom.f PInfty (n + 1)).f ≫
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f
[PROOFSTEP]
simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id, karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f, ←
  HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]
[GOAL]
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
        (_ :
          (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P =
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
              P) ≫
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              N₁ ⋙
                (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).map
          f ≫
        eqToHom
          (_ :
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).obj
                Q =
              (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj Q)
[PROOFSTEP]
ext n
[GOAL]
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 : ℕ
⊢ (HomologicalComplex.Hom.f ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f) n).f =
    (HomologicalComplex.Hom.f
        (eqToHom
            (_ :
              (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P =
                (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                      N₁ ⋙
                        (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                          Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                            (ComplexShape.down ℕ)).obj
                  P) ≫
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).map
              f ≫
            eqToHom
              (_ :
                (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                        N₁ ⋙
                          (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                            Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
                              (ComplexShape.down ℕ)).obj
                    Q =
                  (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj Q))
        n).f
[PROOFSTEP]
dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]
[GOAL]
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 : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app f.f (op [n]) =
    (HomologicalComplex.Hom.f
          (eqToHom
            (_ :
              (karoubiChainComplexEquivalence C ℕ).functor.obj (N₂.obj P) =
                HomologicalComplex.mk (fun i => Karoubi.mk (P.X.obj (op [i])) (HomologicalComplex.Hom.f PInfty i).f)
                  fun i j =>
                  Karoubi.Hom.mk
                    (HomologicalComplex.d
                          ((karoubiChainComplexEquivalence (Karoubi C) ℕ).functor.obj
                            (N₁.obj (KaroubiFunctorCategoryEmbedding.obj P)))
                          i j).f.f))
          n).f ≫
      ((HomologicalComplex.Hom.f PInfty n).f ≫ NatTrans.app f.f (op [n])) ≫
        (HomologicalComplex.Hom.f
            (eqToHom
              (_ :
                (HomologicalComplex.mk (fun i => Karoubi.mk (Q.X.obj (op [i])) (HomologicalComplex.Hom.f PInfty i).f)
                    fun i j =>
                    Karoubi.Hom.mk
                      (HomologicalComplex.d
                            ((karoubiChainComplexEquivalence (Karoubi C) ℕ).functor.obj
                              (N₁.obj (KaroubiFunctorCategoryEmbedding.obj Q)))
                            i j).f.f) =
                  (karoubiChainComplexEquivalence C ℕ).functor.obj (N₂.obj Q)))
            n).f
[PROOFSTEP]
simp only [karoubi_PInfty_f, HomologicalComplex.eqToHom_f, Karoubi.eqToHom_f, assoc, comp_id, PInfty_f_naturality,
  app_p_comp, karoubiChainComplexEquivalence_functor_obj_X_p, N₂_obj_p_f, eqToHom_refl, PInfty_f_naturality_assoc,
  app_comp_p, PInfty_f_idem_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.74447, u_1} C
inst✝ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
⊢ ∀ [inst : IsIso (N₂.map f)], IsIso f
[PROOFSTEP]
intro
  -- The following functor `F` reflects isomorphism because it is
      -- a composition of four functors which reflects isomorphisms.
      -- Then, it suffices to show that `F.map f` is an isomorphism.
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
⊢ IsIso f
[PROOFSTEP]
let F₁ := karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
⊢ IsIso f
[PROOFSTEP]
let F₂ : SimplicialObject (Karoubi C) ⥤ _ := N₁
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
⊢ IsIso f
[PROOFSTEP]
let F₃ := (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
⊢ IsIso f
[PROOFSTEP]
let F₄ := Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
⊢ IsIso f
[PROOFSTEP]
let F := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso f
[PROOFSTEP]
haveI : ReflectsIsomorphisms F₁ := reflectsIsomorphisms_of_full_and_faithful _
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this : ReflectsIsomorphisms F₁
⊢ IsIso f
[PROOFSTEP]
haveI : ReflectsIsomorphisms F₂ := by infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this : ReflectsIsomorphisms F₁
⊢ ReflectsIsomorphisms F₂
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝ : ReflectsIsomorphisms F₁
this : ReflectsIsomorphisms F₂
⊢ IsIso f
[PROOFSTEP]
haveI : ReflectsIsomorphisms F₃ := reflectsIsomorphisms_of_full_and_faithful _
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝¹ : ReflectsIsomorphisms F₁
this✝ : ReflectsIsomorphisms F₂
this : ReflectsIsomorphisms F₃
⊢ IsIso f
[PROOFSTEP]
haveI : ReflectsIsomorphisms ((KaroubiKaroubi.equivalence C).inverse) := reflectsIsomorphisms_of_full_and_faithful _
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝² : ReflectsIsomorphisms F₁
this✝¹ : ReflectsIsomorphisms F₂
this✝ : ReflectsIsomorphisms F₃
this : ReflectsIsomorphisms (KaroubiKaroubi.equivalence C).inverse
⊢ IsIso f
[PROOFSTEP]
have : IsIso (F.map f) := by
  simp only
  rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]
  apply Functor.map_isIso
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝² : ReflectsIsomorphisms F₁
this✝¹ : ReflectsIsomorphisms F₂
this✝ : ReflectsIsomorphisms F₃
this : ReflectsIsomorphisms (KaroubiKaroubi.equivalence C).inverse
⊢ IsIso (F.map f)
[PROOFSTEP]
simp only
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝² : ReflectsIsomorphisms F₁
this✝¹ : ReflectsIsomorphisms F₂
this✝ : ReflectsIsomorphisms F₃
this : ReflectsIsomorphisms (KaroubiKaroubi.equivalence C).inverse
⊢ IsIso
    ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          N₁ ⋙
            (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
              Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)).map
      f)
[PROOFSTEP]
rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝² : ReflectsIsomorphisms F₁
this✝¹ : ReflectsIsomorphisms F₂
this✝ : ReflectsIsomorphisms F₃
this : ReflectsIsomorphisms (KaroubiKaroubi.equivalence C).inverse
⊢ IsIso ((karoubiChainComplexEquivalence C ℕ).functor.map (N₂.map f))
[PROOFSTEP]
apply Functor.map_isIso
[GOAL]
C : Type u_1
inst✝² : Category.{?u.74447, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
this✝³ : ReflectsIsomorphisms F₁
this✝² : ReflectsIsomorphisms F₂
this✝¹ : ReflectsIsomorphisms F₃
this✝ : ReflectsIsomorphisms (KaroubiKaroubi.equivalence C).inverse
this : IsIso (F.map f)
⊢ IsIso f
[PROOFSTEP]
exact isIso_of_reflects_iso f F