[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
