C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 =
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z)))
          (_ :
            {
                      fst :=
                        syzygies
                          { fst := over Z,
                                snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := over Z,
                                    snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                          snd :=
                            (_ :
                              d
                                    { fst := over Z,
                                          snd :=
                                            { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                                0) } }.snd.fst ≫
                { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ ≫
      Projective.π Z
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0 =
    HomologicalComplex.d (ofComplex Z) 1 0 ≫ Projective.π Z
simp only [ofComplex_X, ChainComplex.single₀_obj_X_0, ChainComplex.single₀_obj_X_succ,
  ComplexShape.down_Rel, not_true, ChainComplex.single₀_obj_X_d, comp_zero, ofComplex_d,
  eqToHom_refl, Category.id_comp, dite_eq_ite, ite_true]
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 =
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z)))
          (_ :
            {
                      fst :=
                        syzygies
                          { fst := over Z,
                                snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := over Z,
                                    snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                          snd :=
                            (_ :
                              d
                                    { fst := over Z,
                                          snd :=
                                            { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                                0) } }.snd.fst ≫
                { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ ≫
      Projective.π Z
exact (exact_d_f (Projective.π Z)).w.symm