∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₃' : ι}
  (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₃' : i₂ ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃') (n₀ n₁ n₂ n₃ : ℤ),
  autoParam (α.app 0 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 0))
      CategoryTheory.Abelian.SpectralObject.epi_map._auto_1 →
    autoParam (α.app 1 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 1))
        CategoryTheory.Abelian.SpectralObject.epi_map._auto_3 →
      autoParam (α.app 2 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 2))
          CategoryTheory.Abelian.SpectralObject.epi_map._auto_5 →
        ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.epi_map._auto_7)
          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.epi_map._auto_9),
          autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.epi_map._auto_11 →
            CategoryTheory.Epi (X.map f₁ f₂ f₃ f₁ f₂ f₃' α n₀ n₁ n₂ hn₁ hn₂)