C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫
      (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
          (d (d (Injective.ι Z)))
          (_ :
            { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
                {
                      fst :=
                        syzygies
                          { fst := under Z,
                                snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := under Z,
                                    snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                          snd :=
                            (_ :
                              { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                  d
                                    { fst := under Z,
                                          snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                                0) } }.snd.fst =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ =
    0
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ HomologicalComplex.d (ofCocomplex Z) 0 1 =
    HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1 ≫ 0
simp only [ofCocomplex_d, eq_self_iff_true, eqToHom_refl, Category.comp_id,
  dite_eq_ite, if_true, comp_zero]
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫
      (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
          (d (d (Injective.ι Z)))
          (_ :
            { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
                {
                      fst :=
                        syzygies
                          { fst := under Z,
                                snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := under Z,
                                    snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                          snd :=
                            (_ :
                              { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                  d
                                    { fst := under Z,
                                          snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                                0) } }.snd.fst =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ =
    0
exact (exact_f_d (Injective.ι Z)).w