C : Type ?u.247870
inst✝³ : Category C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f
      (id
        (ChainComplex.ofHom (fun n => underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X)
          (_ : ∀ (n : ℕ), NormalizedMooreComplex.objD X (n + 1) ≫ NormalizedMooreComplex.objD X n = 0)
          (fun n => X.obj [n].op) (AlternatingFaceMapComplex.objD X)
          (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0)
          (fun n => arrow (NormalizedMooreComplex.objX X n))
          (_ :
            ∀ (i : ℕ),
              arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ AlternatingFaceMapComplex.objD X i =
                NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i))))
      n =
    arrow (NormalizedMooreComplex.objX X n)
C : Type ?u.247870
inst✝³ : Category C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) n = arrow (NormalizedMooreComplex.objX X n)
dsimp only [inclusionOfMooreComplexMap]
no goals
C : Type ?u.247870
inst✝³ : Category C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f
      (id
        (ChainComplex.ofHom (fun n => underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X)
          (_ : ∀ (n : ℕ), NormalizedMooreComplex.objD X (n + 1) ≫ NormalizedMooreComplex.objD X n = 0)
          (fun n => X.obj [n].op) (AlternatingFaceMapComplex.objD X)
          (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0)
          (fun n => arrow (NormalizedMooreComplex.objX X n))
          (_ :
            ∀ (i : ℕ),
              arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ AlternatingFaceMapComplex.objD X i =
                NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i))))
      n =
    arrow (NormalizedMooreComplex.objX X n)
exact ChainComplex.ofHom_f _ _ _ _ _ _ _ _ n