awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
hj : coreE₂HomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe (coreE₂HomologicalNat.deg (p, q) + 1)
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂HomologicalNat.deg (p, q) + 1)).obj
      (mk₁ (X₀ := coreE₂HomologicalNat.i₀ (r + 1) (p, q) ⋯) (X₁ := coreE₂HomologicalNat.i₀ r (p, q) ⋯)
        (homOfLE ⋯ : coreE₂HomologicalNat.i₀ (r + 1) (p, q) ⋯ ⟶ coreE₂HomologicalNat.i₀ r (p, q) ⋯)))

Tactic:
apply isZero₂_of_isThirdQuadrant

Premises used: CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
hj : -(↑q : ℤ) - r + 2 ≤ HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1
⊢ coreE₂HomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe (coreE₂HomologicalNat.deg (p, q) + 1)

Tactic:
simp only [coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_deg, WithBotTop.coe_le_coe]

Premises used: CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg, WithBotTop.coe_le_coe, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
hj : ∀ (this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2), False
⊢ -(↑q : ℤ) - r + 2 ≤ HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1

Tactic:
by_contra!
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
⊢ 0 ≤ (↑p : ℤ) - r

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
hj : ∀ (p' : ℕ) (hp' : (↑p : ℤ) - r = (↑p' : ℤ)), False
⊢ False

Tactic:
obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p - r by lia)

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
⊢ 0 ≤ (↑q : ℤ) + r - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
hj : ∀ (q' : ℕ) (hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)), False
⊢ False

Tactic:
obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + r - 1 by lia)

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)
left : (↑(p, q).1 : ℤ) + (-r, r - 1).1 = (↑(p', q').1 : ℤ)
right : (↑(p, q).2 : ℤ) + (-r, r - 1).2 = (↑(p', q').2 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) (p', q')

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)
⊢ (↑(p, q).1 : ℤ) + (-r, r - 1).1 = (↑(p', q').1 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)
⊢ (↑(p, q).2 : ℤ) + (-r, r - 1).2 = (↑(p', q').2 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)
⊢ False

Tactic:
exact hpq ⟨p', q'⟩ (by constructor <;> lia)

Premises used: Prod.mk
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
hi : WithBotTop.coe 0 < coreE₂HomologicalNat.i₃ r (p, q) ⋯
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂HomologicalNat.deg (p, q) - 1)).obj
      (mk₁ (X₀ := coreE₂HomologicalNat.i₃ r (p, q) ⋯) (X₁ := coreE₂HomologicalNat.i₃ (r + 1) (p, q) ⋯)
        (homOfLE ⋯ : coreE₂HomologicalNat.i₃ r (p, q) ⋯ ⟶ coreE₂HomologicalNat.i₃ (r + 1) (p, q) ⋯)))

Tactic:
apply isZero₁_of_isThirdQuadrant

Premises used: CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
hi : 0 < -(↑q : ℤ) + r - 1
⊢ WithBotTop.coe 0 < coreE₂HomologicalNat.i₃ r (p, q) ⋯

Tactic:
simp only [coreE₂HomologicalNat_i₃, WithBotTop.coe_lt_coe]

Premises used: CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃, WithBotTop.coe_lt_coe
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
hi : ∀ (this : -(↑q : ℤ) + r - 1 ≤ 0), False
⊢ 0 < -(↑q : ℤ) + r - 1

Tactic:
by_contra!
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
⊢ 0 ≤ (↑p : ℤ) + r

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
hi : ∀ (p' : ℕ) (hp' : (↑p : ℤ) + r = (↑p' : ℤ)), False
⊢ False

Tactic:
obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p + r by lia)

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
⊢ 0 ≤ HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
hi : ∀ (q' : ℕ) (hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)), False
⊢ False

Tactic:
obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + 1 - r by lia)

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
left : (↑(p', q').1 : ℤ) + (-r, r - 1).1 = (↑(p, q).1 : ℤ)
right : (↑(p', q').2 : ℤ) + (-r, r - 1).2 = (↑(p, q).2 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p', q') (p, q)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
⊢ (↑(p', q').1 : ℤ) + (-r, r - 1).1 = (↑(p, q).1 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
⊢ (↑(p', q').2 : ℤ) + (-r, r - 1).2 = (↑(p, q).2 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
⊢ False

Tactic:
exact hpq ⟨p', q'⟩ (by constructor <;> lia)

Premises used: Prod.mk
-- 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₃
⊢ Epi (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ h h_1 h_2).g

Tactic:
inferInstanceAs (Epi (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) ..))

Premises used: _private.0.CategoryTheory.Abelian.SpectralObject.instEpiGDCokernelSequence._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.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂),
    x₂ ≫ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₁),
        π ≫ x₂ = x₁ ≫ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f
⊢ (X.dCokernelSequence 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.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ (X.dCokernelSequence 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.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₁),
    π ≫ x₂ = x₁ ≫ (X.dCokernelSequence 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.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
⊢ CategoryStruct.comp (Y := 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₃ ⋯ ⋯) (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) 0 (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯)

Tactic:
have hx₂' := hx₂ =≫ 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.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₂' :
  CategoryStruct.comp (Y := 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₃ ⋯ ⋯) (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) 0 (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₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0

Tactic:
rw [assoc, zero_comp, X.map_ιE f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄)
    (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄) n₁ n₂ n₃] at hx₂'

Premises used: CategoryTheory.ComposableArrows.fourδ₄Toδ₃, CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.threeδ₃Toδ₂, CategoryTheory.Abelian.SpectralObject.map_ιE, CategoryTheory.Limits.zero_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₃₄
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₂' :
  CategoryStruct.comp (Y := 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₃ ⋯ ⋯) (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) 0 (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯)
hx₂'₁ : 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
⊢ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0

Tactic:
rw [assoc, zero_comp, X.map_ιE f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄)
    (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄) n₁ n₂ n₃] at hx₂'

Premises used: CategoryTheory.ComposableArrows.fourδ₄Toδ₃, CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.threeδ₃Toδ₂, CategoryTheory.Abelian.SpectralObject.map_ιE, CategoryTheory.Limits.zero_comp