{V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : ChainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 0 ⟶ Q.X 1) →
            (one : P.X 1 ⟶ Q.X 2) →
              e.f 1 =
                  CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1) →
                ((n : ℕ) →
                    (p :
                        (f : P.X n ⟶ Q.X (n + 1)) ×'
                          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                            e.f (n + 1) =
                              CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                                CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
                      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
                        e.f (n + 2) =
                          CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
                            CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) →
                  (n : ℕ) →
                    (f : P.X n ⟶ Q.X (n + 1)) ×'
                      (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                        e.f (n + 1) =
                          CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                            CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))