-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.mk.injEq : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (H : ℤ → CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C)
  (δ' :
    (n₀ n₁ : ℤ) →
      n₀ + 1 = n₁ →
        ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_2
                CategoryTheory.Abelian.SpectralObject._proof_4).comp
            (H n₀) ⟶
          (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Abelian.SpectralObject._proof_6
                CategoryTheory.Abelian.SpectralObject._proof_2).comp
            (H n₁)))
  (exact₁' :
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂ ((δ' n₀ n₁ h).app D)
          ((H n₁).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8
                  CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))).Exact)
  (exact₂' :
    ∀ (n : ℤ) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂
          ((H n).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8
                  CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))
          ((H n).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))).Exact)
  (exact₃' :
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂
          ((H n₀).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))
          ((δ' n₀ n₁ h).app D)).Exact)
  (H_1 : ℤ → CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C)
  (δ'_1 :
    (n₀ n₁ : ℤ) →
      n₀ + 1 = n₁ →
        ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_2
                CategoryTheory.Abelian.SpectralObject._proof_4).comp
            (H_1 n₀) ⟶
          (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Abelian.SpectralObject._proof_6
                CategoryTheory.Abelian.SpectralObject._proof_2).comp
            (H_1 n₁)))
  (exact₁'_1 :
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂ ((δ'_1 n₀ n₁ h).app D)
          ((H_1 n₁).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8
                  CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))).Exact)
  (exact₂'_1 :
    ∀ (n : ℤ) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂
          ((H_1 n).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8
                  CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))
          ((H_1 n).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))).Exact)
  (exact₃'_1 :
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂
          ((H_1 n₀).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))
          ((δ'_1 n₀ n₁ h).app D)).Exact),
  ({ H := H, δ' := δ', exact₁' := exact₁', exact₂' := exact₂', exact₃' := exact₃' } =
      { H := H_1, δ' := δ'_1, exact₁' := exact₁'_1, exact₂' := exact₂'_1, exact₃' := exact₃'_1 }) =
    (H = H_1 ∧ δ' ≍ δ'_1)