awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
φ : X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯ ⟶
  X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯ :=
  { τ₁ := X.pOpcycles f₁ f₂₃ n₁, τ₂ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂,
    τ₃ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
rw : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).Exact
⊢ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
φ : X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯ ⟶
  X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯ :=
  { τ₁ := X.pOpcycles f₁ f₂₃ n₁, τ₂ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂,
    τ₃ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).Exact

Tactic:
X.cokernelSequenceOpcyclesE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂

Premises used: CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
φ : X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯ ⟶
  X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯ :=
  { τ₁ := X.pOpcycles f₁ f₂₃ n₁, τ₂ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂,
    τ₃ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).Exact

Tactic:
exact X.cokernelSequenceOpcyclesE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂

Premises used: CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : Eq (α := (mk₂ f₁₂ f₃).obj 0 ⟶ (mk₂ f₁₂' f₃').obj 0) (β.app 0) (α.app 0)
h₁ : Eq (α := (mk₂ f₁₂ f₃).obj 1 ⟶ (mk₂ f₁₂' f₃').obj 1) (β.app 1) (α.app 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  (X.H n₁).map
        (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
          homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
            (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯) ≫
      X.pOpcycles f₂' f₃' n₁ =
    (X.H n₁).map
        (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
          (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯)) ≫
      X.pOpcycles f₂' f₃' n₁
⊢ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ ≫ X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯ =
    X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁ ≫ X.opcyclesToE f₁' f₂' f₃' f₁₂' h₁₂' n₀ n₁ n₂ hn₁ hn₂

Tactic:
rw [← cancel_mono (X.ιE ..), Category.assoc, Category.assoc, opcyclesToE_ιE ..,
    ← cancel_epi (X.pOpcycles ..), p_opcyclesToE_assoc ..,
    X.πE_map_assoc _ _ _ _ _ _ _
      (homMk₂ (α.app 0) (α.app 1) (α.app 2) (naturality' α 0 1) (naturality' α 1 2)) ..,
    πE_ιE .., X.cyclesMap_i_assoc .., toCycles_i_assoc,
    X.p_opcyclesMap_assoc .., X.p_opcyclesMap ..,
    ← Functor.map_comp_assoc, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.πE_ιE, CategoryTheory.Abelian.SpectralObject.πE_map_assoc, CategoryTheory.cancel_mono, CategoryTheory.ComposableArrows.naturality', CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap, CategoryTheory.Abelian.SpectralObject.ιE, CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE, CategoryTheory.Abelian.SpectralObject.p_opcyclesToE_assoc, OfNat.ofNat, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc, CategoryTheory.ComposableArrows.homMk₂, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.SpectralObject.pOpcycles, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : Eq (α := (mk₂ f₁₂ f₃).obj 0 ⟶ (mk₂ f₁₂' f₃').obj 0) (β.app 0) (α.app 0)
h₁ : Eq (α := (mk₂ f₁₂ f₃).obj 1 ⟶ (mk₂ f₁₂' f₃').obj 1) (β.app 1) (α.app 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
e_a :
  Eq (α := mk₁ f₁₂ ⟶ mk₁ f₂')
    (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
      homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
        (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯)
    (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
      (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯))
⊢ (X.H n₁).map
        (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
          homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
            (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯) ≫
      X.pOpcycles f₂' f₃' n₁ =
    (X.H n₁).map
        (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
          (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯)) ≫
      X.pOpcycles f₂' f₃' n₁

Tactic:
congr 2
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : Eq (α := (mk₂ f₁₂ f₃).obj 0 ⟶ (mk₂ f₁₂' f₃').obj 0) (β.app 0) (α.app 0)
h₁ : Eq (α := (mk₂ f₁₂ f₃).obj 1 ⟶ (mk₂ f₁₂' f₃').obj 1) (β.app 1) (α.app 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
e_a :
  Eq (α := (mk₁ f₁₂).obj' 0 homMk₁._proof_4 ⟶ (mk₁ f₂').obj' 0 homMk₁._proof_4)
    (app'
      (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
        homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
          (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯)
      0 homMk₁._proof_4)
    (app'
      (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
        (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯))
      0 homMk₁._proof_4)
e_a₁ :
  Eq (α := (mk₁ f₁₂).obj' 1 homMk₁._proof_5 ⟶ (mk₁ f₂').obj' 1 homMk₁._proof_5)
    (app'
      (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
        homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
          (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯)
      1 homMk₁._proof_5)
    (app'
      (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
        (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯))
      1 homMk₁._proof_5)
⊢ Eq (α := mk₁ f₁₂ ⟶ mk₁ f₂')
    (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
      homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
        (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯)
    (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
      (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯))

Tactic:
ext
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : Eq (α := (mk₂ f₁₂ f₃).obj 0 ⟶ (mk₂ f₁₂' f₃').obj 0) (β.app 0) (α.app 0)
h₁ : Eq (α := (mk₂ f₁₂ f₃).obj 1 ⟶ (mk₂ f₁₂' f₃').obj 1) (β.app 1) (α.app 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (mk₁ f₁₂).obj' 0 homMk₁._proof_4 ⟶ (mk₁ f₂').obj' 0 homMk₁._proof_4)
    (app'
      (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
        homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
          (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯)
      0 homMk₁._proof_4)
    (app'
      (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
        (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯))
      0 homMk₁._proof_4)

Tactic:
simpa [h₀] using naturality' α 0 1

Premises used: CategoryTheory.ComposableArrows.naturality', OfNat.ofNat
-- 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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : Eq (α := (mk₂ f₁₂ f₃).obj 0 ⟶ (mk₂ f₁₂' f₃').obj 0) (β.app 0) (α.app 0)
h₁ : Eq (α := (mk₂ f₁₂ f₃).obj 1 ⟶ (mk₂ f₁₂' f₃').obj 1) (β.app 1) (α.app 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (mk₁ f₁₂).obj' 1 homMk₁._proof_5 ⟶ (mk₁ f₂').obj' 1 homMk₁._proof_5)
    (app'
      (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
        homMk₁ (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 1)
          (NatTrans.app (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) 2) ⋯)
      1 homMk₁._proof_5)
    (app'
      (CategoryStruct.comp (Y := mk₁ f₁₂') (homMk₁ (β.app 0) (β.app 1) ⋯)
        (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯))
      1 homMk₁._proof_5)

Tactic:
simp [h₁]
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq : κ
i₀ i₁ i₂ i₃ : ι
h₀ : i₀ = data.i₀ r pq ⋯
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h₃ : i₃ = data.i₃ r pq ⋯
n₀ n₁ n₂ : ℤ
h : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₀ = n₁ - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq : κ
i₀ i₁ i₂ i₃ : ι
h₀ : i₀ = data.i₀ r pq ⋯
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h₃ : i₃ = data.i₃ r pq ⋯
n₀ n₁ n₂ : ℤ
h : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
obtain :
  ∀ (hn₁ : n₁ - 1 + 1 = n₁), pageX X data r pq hr = X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂
⊢ pageX X data r pq hr = X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂

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

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq : κ
i₀ i₁ i₂ i₃ : ι
h₀ : i₀ = data.i₀ r pq ⋯
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h₃ : i₃ = data.i₃ r pq ⋯
n₁ n₂ : ℤ
h : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
subst :
  ∀ (hn₁ : data.deg pq - 1 + 1 = data.deg pq),
    pageX X data r pq hr =
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) hn₁ ⋯
⊢ pageX X data r pq hr = X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
subst h hn₂ h₀ h₁ h₂ h₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq : κ
hn₁ : data.deg pq - 1 + 1 = data.deg pq
⊢ pageX X data r pq hr = X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) hn₁ ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_3
rw : data.i₀ r pq ⋯ = data.i₂ pq'
rw₁ rw₂ : data.i₂ pq' = data.i₂ pq'
⊢ i₂ = data.i₂ pq'

Tactic:
rw [h₂, data.hc₀₂ r pq pq' hpq]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_3
rw : data.i₁ pq = data.i₃ r pq' ⋯
rw₁ rw₂ : data.i₃ r pq' ⋯ = data.i₃ r pq' ⋯
⊢ i₃ = data.i₃ r pq' ⋯

Tactic:
rw [h₃, data.hc₁₃ r pq pq' hpq]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_3
⊢ n₂ = data.deg pq'

Tactic:
simpa only [← hn₂, hn₁'] using data.hc r pq pq' hpq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
subst :
  ∀ (hn₁ : n₀ + 1 = data.deg pq) (hn₂ : data.deg pq + 1 = n₂) (f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
    (f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (f₄ : data.i₁ pq ⟶ data.i₂ pq)
    (f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯),
    Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯) (pageD X data r pq pq' ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ (data.deg pq)
            n₂ ⋯ hn₁ hn₂) ≫
        X.d f₁ f₂ f₃ f₄ f₅ n₀ (data.deg pq) n₂ n₃ hn₁ hn₂ hn₃ ≫
          Iso.inv
            (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              n₂ n₃ ⋯ hn₂ hn₃))
⊢ Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯) (pageD X data r pq pq' ⋯)
    (Iso.hom (pageXIso X data r ⋯ pq i₂ i₃ i₄ i₅ h₂ h₃ h₄ h₅ n₀ n₁ n₂ hn₁' hn₁ hn₂) ≫
      X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫
        Iso.inv (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ h₀ h₁ ⋯ ⋯ n₁ n₂ n₃ ⋯ hn₂ hn₃))

Tactic:
subst hn₁' h₀ h₁ h₂ h₃ h₄ h₅
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₀ n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₁ : n₀ + 1 = data.deg pq
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
⊢ n₀ = data.deg pq - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₀ n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₁ : n₀ + 1 = data.deg pq
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
obtain :
  ∀ (hn₁ : data.deg pq - 1 + 1 = data.deg pq),
    Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯) (pageD X data r pq pq' ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) n₂ ⋯ hn₁ hn₂) ≫
        X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) n₂ n₃ hn₁ hn₂ hn₃ ≫
          Iso.inv
            (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              n₂ n₃ ⋯ hn₂ hn₃))
⊢ Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯) (pageD X data r pq pq' ⋯)
    (Iso.hom
        (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ (data.deg pq) n₂
          ⋯ hn₁ hn₂) ≫
      X.d f₁ f₂ f₃ f₄ f₅ n₀ (data.deg pq) n₂ n₃ hn₁ hn₂ hn₃ ≫
        Iso.inv
          (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
            n₂ n₃ ⋯ hn₂ hn₃))

Tactic:
obtain rfl : n₀ = data.deg pq - 1 := by lia

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
⊢ n₂ = data.deg pq + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
obtain :
  ∀ (hn₃ : data.deg pq + 1 + 1 = n₃) (hn₂ : data.deg pq + 1 = data.deg pq + 1),
    Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯) (pageD X data r pq pq' ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) ⋯ hn₁ hn₂) ≫
        X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) n₃ hn₁ hn₂ hn₃ ≫
          Iso.inv
            (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) n₃ ⋯ hn₂ hn₃))
⊢ Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯) (pageD X data r pq pq' ⋯)
    (Iso.hom
        (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
          (data.deg pq) n₂ ⋯ hn₁ hn₂) ≫
      X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) n₂ n₃ hn₁ hn₂ hn₃ ≫
        Iso.inv
          (pageXIso X data r ⋯ pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
            n₂ n₃ ⋯ hn₂ hn₃))

Tactic:
obtain rfl : n₂ = data.deg pq + 1 := by lia

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg, rfl