awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
⊢ (x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) ≫ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).g = 0

Tactic:
simp [sequenceΨ, Precomp.map, hx₂']

Premises used: CategoryTheory.Abelian.SpectralObject.sequenceΨ, CategoryTheory.ComposableArrows.Precomp.map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
    Epi π₁ →
      ∀ (x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁)
        (hx₁ :
          π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).f),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
          π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    ((X.sequenceΨ_exact f₂ f₃ f₄ _ rfl f₃₄ h₃₄ n₁ n₂).exact 1).exact_up_to_refinements
      (x₂ ≫ X.ιE ..) (by simp [sequenceΨ, Precomp.map, hx₂'])

Premises used: CategoryTheory.Abelian.SpectralObject.sequenceΨ_exact, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.Abelian.SpectralObject.ιE, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
⟨A₁, π₁, inferInstance, x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂, ?_⟩

Premises used: inferInstance, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Abelian.SpectralObject.πE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
refine :
  π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
refine ⟨A₁, π₁, inferInstance, x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂, ?_⟩
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂'_1 : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
rw :
  (π₁ ≫ x₂) ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₁ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯))
      (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯)
rw₂ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
rw₃ :
  π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    x₁ ≫
      CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
          (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
rw₄ :
  x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯ =
    x₁ ≫
      CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
        (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
          (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
rw₅ rw₆ : x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯ = x₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
⊢ π₁ ≫ x₂ =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (x₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)

Tactic:
rw [← cancel_mono (X.ιE ..), assoc, assoc, assoc, hx₁, πE_d_ιE ..]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.ιE, CategoryTheory.Abelian.SpectralObject.πE_d_ιE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₅ 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₃ : ℤ
h : n₀ + 1 = n₁
h_1 : n₁ + 1 = n₂
h_2 : n₂ + 1 = n₃
⊢ Mono (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ h h_1 h_2).f

Tactic:
inferInstanceAs (Mono (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃) ..))

Premises used: _private.0.CategoryTheory.Abelian.SpectralObject.instMonoFDKernelSequence._proof_1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
rw :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂),
    x₂ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₁),
        π ≫ x₂ = x₁ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f
⊢ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0
dsimp :
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₁),
    π ≫ x₂ = x₁ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f

Tactic:
dsimp at hx₂ ⊢
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
    Epi π₁ →
      ∀ (y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁) (hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
          π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
obtain ⟨A₁, π₁, _, y₂, hy₂⟩ :=
    surjective_up_to_refinements_of_epi (X.πE f₃ f₄ f₅ n₀ n₁ n₂) x₂

Premises used: CategoryTheory.surjective_up_to_refinements_of_epi, CategoryTheory.Abelian.SpectralObject.πE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
⊢ (π₁ ≫ x₂) ≫
      CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))

Tactic:
have hy₂' := hy₂ =≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ≫ X.ιE ..
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' :
  (π₁ ≫ x₂) ≫
      CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) (y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯)
        (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯))
⊢ 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯

Tactic:
simp only [assoc, reassoc_of% hx₂, zero_comp, comp_zero, πE_d_ιE] at hy₂'

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, CategoryTheory.Abelian.SpectralObject.πE_d_ιE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
obtain :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
    Epi π₂ →
      ∀ (y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁)
        (hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
          π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
obtain ⟨A₂, π₂, _, y₁, hy₁⟩ :=
    ((X.sequenceΨ_exact f₂ f₃ f₄ f₂₃ h₂₃ _ rfl n₁ n₂).exact 0).exact_up_to_refinements y₂ hy₂'.symm

Premises used: CategoryTheory.Abelian.SpectralObject.sequenceΨ_exact, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, OfNat.ofNat, Eq.symm, CategoryTheory.ComposableArrows.Exact.exact, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁
hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
⟨A₂, π₂ ≫ π₁, inferInstance, y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂, ?_⟩

Premises used: inferInstance, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Abelian.SpectralObject.πE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁
hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f
refine :
  (π₂ ≫ π₁) ≫ x₂ =
    (y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
refine ⟨A₂, π₂ ≫ π₁, inferInstance, y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂, ?_⟩
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁
hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f
⊢ (π₂ ≫ π₁) ≫ x₂ =
    (y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
simp [sequenceΨ, hy₂, reassoc_of% hy₁, X.πE_map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃)
    (threeδ₁Toδ₀ f₂ f₃ f₄ f₂₃) n₀ n₁ n₂]

Premises used: CategoryTheory.ComposableArrows.fourδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.sequenceΨ, CategoryTheory.ComposableArrows.threeδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.πE_map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₂₃
f₅₆ : i₄ ⟶ i₆
h₅₆ : f₅ ≫ f₆ = f₅₆
n₁ n₂ n₃ : ℤ
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
simp :
  Eq (α := X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯ ⟶ X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯ ≫ fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯ ≫ fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)
⊢ Eq (α := X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯ ⟶ X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯ ≫
      X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯ ≫
      X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)

Tactic:
simp only [← map_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.map_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Homology
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₂₃
f₅₆ : i₄ ⟶ i₆
h₅₆ : f₅ ≫ f₆ = f₅₆
n₁ n₂ n₃ : ℤ
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α := X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯ ⟶ X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯ ≫ fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯ ≫ fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)
⊢ Eq (α := X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯ ⟶ X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯ ≫ fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯ ≫ fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X.H n₁).obj (mk₁ f₂))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsZero.{v_1, u_1} (X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

Tactic:
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).exact_iff_isZero_homology.1
    (ShortComplex.exact_of_isZero_X₂ _ h)

Premises used: CategoryTheory.Abelian.SpectralObject.E, CategoryTheory.ShortComplex.exact_iff_isZero_homology, CategoryTheory.Abelian.SpectralObject.shortComplex, Iff.mp, CategoryTheory.ShortComplex.exact_of_isZero_X₂