-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.mk.inj : ∀ {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