[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
let F : SimplicialObject A ⥤ _ := Idempotents.DoldKan.N
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
F : SimplicialObject A ⥤ ChainComplex A ℕ := Idempotents.DoldKan.N
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
let hF : IsEquivalence F := IsEquivalence.ofEquivalence Idempotents.DoldKan.equivalence
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
F : SimplicialObject A ⥤ ChainComplex A ℕ := Idempotents.DoldKan.N
hF : IsEquivalence F := IsEquivalence.ofEquivalence Idempotents.DoldKan.equivalence
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
letI : IsEquivalence (N : SimplicialObject A ⥤ _) := IsEquivalence.ofIso comparisonN.symm hF
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
F : SimplicialObject A ⥤ ChainComplex A ℕ := Idempotents.DoldKan.N
hF : IsEquivalence F := IsEquivalence.ofEquivalence Idempotents.DoldKan.equivalence
this : IsEquivalence N := IsEquivalence.ofIso comparisonN.symm hF
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
exact N.asEquivalence
