awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
obtain :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
    Epi π₂ →
      ∀ (z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁)
        (hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
          A' ⟶
            { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
          π ≫ z₀ =
            x₁ ≫
              { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                  f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                  zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z₀ =
      x₁ ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.f

Tactic:
obtain ⟨A₂, π₂, _, z₂, hz₂⟩ :=
      (X.cokernelSequenceOpcycles_exact f₁ f₂₃ n₀ n₁ hn₁).exact_up_to_refinements z₁ (by
    dsimp
    have H := X.p_opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) (𝟙 _) n₁ (by cat_disch)
    rw [Functor.map_id, id_comp] at H
    rw [← H, ← reassoc_of% hz₁, hz₀, comp_zero])

Premises used: CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_exact, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z₀ =
      x₁ ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.f

Tactic:
⟨A₂, π₂ ≫ π₁, inferInstance, z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀, ?_⟩

Premises used: inferInstance, CategoryTheory.Abelian.SpectralObject.toCycles, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
refine :
  (π₂ ≫ π₁) ≫ z₀ =
    (z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z₀ =
      x₁ ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.f

Tactic:
refine ⟨A₂, π₂ ≫ π₁, inferInstance, z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀, ?_⟩
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sequenceΨ f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁).Exact

Tactic:
exact_of_δ₀ (X.cyclesMap_Ψ_exact f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁).exact_toComposableArrows
    (X.Ψ_opcyclesMap_exact f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁).exact_toComposableArrows

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_exact, CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap_exact, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ComposableArrows.exact_of_δ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₂ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₃ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₄ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₅ :
  (X.H n₁).map (𝟙 (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₆ :
  𝟙 ((X.H n₁).obj (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₇ rw₈ : X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ = X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂

Tactic:
rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, CategoryTheory.Abelian.SpectralObject.πE_ιE, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.CategoryStruct.comp, CategoryTheory.Abelian.SpectralObject.toCycles_Ψ, CategoryTheory.cancel_epi, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, rfl, CategoryTheory.Category.id_comp, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₀ = n₁ - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
obtain :
  ∀ (hn₁ : n₁ - 1 + 1 = n₁),
    X.πE (𝟙 i₀) f₁ (𝟙 i₁) (n₁ - 1) n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ (n₁ - 1) n₁ n₂ hn₁ hn₂).hom =
      (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom
⊢ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom = (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ X.πE (𝟙 i₀) f₁ (𝟙 i₁) (n₁ - 1) n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ (n₁ - 1) n₁ n₂ hn₁ hn₂).hom =
    (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom

Tactic:
simp [πE, cyclesIsoH, EIsoH]

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesIsoH, CategoryTheory.Abelian.SpectralObject.EIsoH, CategoryTheory.Abelian.SpectralObject.πE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 𝟙 i₁ ≫ f₂ = f₂

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 𝟙 i₀ ≫ f₁ = f₁

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₂ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫
      X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₃ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₄ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₅ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ 𝟙 ((X.H n₂).obj (mk₁ f₁)) =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₆ : X.δ f₁ f₂ n₁ n₂ hn₂ = X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₇ rw₈ : X.δ f₁ f₂ n₁ n₂ hn₂ = X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂

Tactic:
rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]

Premises used: CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom_assoc, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.Abelian.SpectralObject.πE, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw : Epi.{v_1, u_1} (𝟙 (X.cycles f₁ f₂ n₁))
⊢ Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)

Tactic:
rw [X.cyclesMap_id]

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesMap_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi.{v_1, u_1} (𝟙 (X.cycles f₁ f₂ n₁))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀' i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₁' : i₀' ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.opcycles f₂ f₃ n₁)
    (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
    (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃ (𝟙 (mk₂ f₂ f₃)) n₁)

Tactic:
have := X.map_ιE _ _ _ _ _ _ α (𝟙 _) n₀ n₁ n₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀' i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₁' : i₀' ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.opcycles f₂ f₃ n₁)
    (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
    (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃ (𝟙 (mk₂ f₂ f₃)) n₁)
⊢ Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.opcycles f₂ f₃ n₁)
    (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

Tactic:
rw [opcyclesMap_id, comp_id] at this

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Abelian.SpectralObject.opcyclesMap_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀' i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₁' : i₀' ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.opcycles f₂ f₃ n₁)
    (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
mono_of_mono_fac this

Premises used: CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀' i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₁' : i₀' ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.opcycles f₂ f₃ n₁)
    (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
exact mono_of_mono_fac this

Premises used: CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫
      X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃ =
    0

Tactic:
simp [← cancel_epi (X.πE f₃ f₄ f₅ n₀ n₁ n₂), ← cancel_epi (X.toCycles f₃ f₄ f₃₄ h₃₄ n₁),
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl f₃₄ h₃₄ n₀ n₁ n₂ n₃,
    X.πE_map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) (𝟙 _) n₁ n₂ n₃]

Premises used: CategoryTheory.ComposableArrows.fourδ₄Toδ₃, CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.Abelian.SpectralObject.πE, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.πE_map, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
ι' : Type u_3
κ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
inst_3 : Preorder ι'
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

Tactic:
X.epi_map _ _ _ _ _ _ _ _ _ rfl rfl rfl hn₂ hn₃ rfl

Premises used: CategoryTheory.Abelian.SpectralObject.epi_map, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
h₁ :
  Epi (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₁)
h₂ :
  IsIso (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₂) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₂)
h₃ :
  Mono (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₃) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₃)
⊢ IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

Tactic:
apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'

Premises used: CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'