awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃ : ℤ
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
hn₃ : data.deg pq + 1 + 1 = n₃
hn₂ : data.deg pq + 1 = data.deg pq + 1
⊢ n₃ = data.deg pq + 2

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₃ : ℤ
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
hn₃ : data.deg pq + 1 + 1 = n₃
hn₂ : data.deg pq + 1 = data.deg pq + 1
obtain :
  ∀ (hn₃ : data.deg pq + 1 + 1 = data.deg pq + 2),
    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) (data.deg pq + 2) 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) (data.deg pq + 2) ⋯ 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) (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₃))

Tactic:
obtain rfl : n₃ = data.deg pq + 2 := 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'
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
hn₂ : data.deg pq + 1 = data.deg pq + 1
hn₃ : data.deg pq + 1 + 1 = data.deg pq + 2
dsimp :
  Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯)
    (if hpq : (c r).Rel pq pq' then
      CategoryStruct.comp (Y :=
        X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
          (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
          (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
              (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
            X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (eqToHom ⋯ :
          X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
            pageX X data r pq' ⋯)
    else 0)
    (𝟙 (pageX X data r pq ⋯) ≫
      X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) hn₁ hn₂ hn₃ ≫ eqToHom ⋯)
⊢ 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) (data.deg pq + 2) 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) (data.deg pq + 2) ⋯ hn₂ hn₃))

Tactic:
dsimp [pageD, pageXIso]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD
-- 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'
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
hn₂ : data.deg pq + 1 = data.deg pq + 1
hn₃ : data.deg pq + 1 + 1 = data.deg pq + 2
⊢ Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯)
    (CategoryStruct.comp (Y :=
        X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
          (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
          (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
              (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
            X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (eqToHom ⋯ :
          X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
            pageX X data r pq' ⋯) :
      pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯)
    (X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) hn₁ hn₂ hn₃ ≫ eqToHom ⋯ :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) hn₁ hn₂ ⟶
        pageX X data r pq' ⋯)

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' pq'' : κ
pos : ∀ (hpq : (c r).Rel pq pq'), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
neg : ∀ (hpq : ¬(c r).Rel pq pq'), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0

Tactic:
by_cases hpq : (c r).Rel pq pq'

Premises used: ComplexShape.Rel
-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
pos : ∀ (hpq' : (c r).Rel pq' pq''), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
neg : ∀ (hpq' : ¬(c r).Rel pq' pq''), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0

Tactic:
by_cases hpq' : (c r).Rel pq' pq''

Premises used: ComplexShape.Rel
-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
⊢ data.deg pq + 1 + 1 = data.deg pq + 2

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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
neg :
  Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0

Tactic:
dsimp only [pageD]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD
-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
neg :
  Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      0)
    0
neg₁ neg₂ : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr) 0 0
⊢ Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0

Tactic:
rw [dif_neg hpq', comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, dif_neg
-- 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' pq'' : κ
hpq : ¬(c r).Rel pq pq'
neg :
  Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0

Tactic:
dsimp only [pageD]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD
-- 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' pq'' : κ
hpq : ¬(c r).Rel pq pq'
neg :
  Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr) 0
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
neg₁ neg₂ : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr) 0 0
⊢ Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0

Tactic:
rw [dif_neg hpq, zero_comp]

Premises used: dif_neg, CategoryTheory.Limits.zero_comp
-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.i₃ r pq'' ⋯ ≤ data.i₀ r pq ⋯

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

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂, 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.deg pq + 1 = data.deg pq'

Tactic:
have := data.hc r pq pq' hpq
-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
this : data.deg pq + 1 = data.deg pq'
⊢ n₁ = data.deg pq

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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
rw rw₁ : data.i₂ pq'' = data.i₂ pq''
⊢ data.i₂ pq'' = data.i₀ r pq' ⋯

Tactic:
rw [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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
rw rw₁ : data.i₃ r pq'' ⋯ = data.i₃ r pq'' ⋯
⊢ data.i₃ r pq'' ⋯ = data.i₁ pq'

Tactic:
rw [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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
rw rw₁ : data.i₂ pq' = data.i₂ pq'
⊢ data.i₀ r pq ⋯ = data.i₂ pq'

Tactic:
rw [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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
rw rw₁ : data.i₃ r pq' ⋯ = data.i₃ r pq' ⋯
⊢ data.i₁ pq = data.i₃ r pq' ⋯

Tactic:
rw [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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.deg pq' + 1 = data.deg pq''

Tactic:
have := data.hc r pq' pq'' hpq'
-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
this : data.deg pq' + 1 = data.deg pq''
⊢ n₃ = data.deg pq''

Tactic:
lia