∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (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)))
  (i j : ℕ),
  ¬(ComplexShape.down ℕ).Rel j i →
    (if h : i + 1 = j then
        CategoryTheory.CategoryStruct.comp (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst
          (HomologicalComplex.xPrevIso Q h).hom
      else 0) =
      0