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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
h : (↑l : ℤ) < (↑q : ℤ) + r
⊢ l ≤ ((↑q : ℤ) + r).toNat

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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
h : (↑l : ℤ) < (↑q : ℤ) + r
rw : Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + r).toNat l
rw₁ : Fin.last l = Fin.clamp ((↑q : ℤ) + r).toNat l
rw₂ rw₃ : Fin.last l = Fin.last l
⊢ Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + (r + 1 - 1)).toNat l

Tactic:
rw [add_sub_cancel_right, Fin.clamp_eq_last _ _ (by lia), Fin.clamp_eq_last _ _ (by lia)]

Premises used: add_sub_cancel_right, Fin.clamp_eq_last
-- 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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ r' pq ⋯

Tactic:
have : (coreE₂CohomologicalFin l).i₃ r pq = (coreE₂CohomologicalFin l).i₃ r' pq := by
      subst hrr'
      obtain ⟨p, q, hq⟩ := pq
      have h : l < q + r := by
        by_contra!
        obtain ⟨t, ht⟩ := Int.le.dest this
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        exact hpq (p - r) ⟨l - 1 - t, by lia⟩ (by lia) (by lia)
      dsimp
      rw [add_sub_cancel_right, Fin.clamp_eq_last _ _ (by lia), Fin.clamp_eq_last _ _ (by 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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
this : (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ r' pq ⋯
⊢ IsIso (homOfLE ⋯)

Tactic:
have := isIso_homOfLE this
-- 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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
this_1 : (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ r' pq ⋯
this : IsIso (homOfLE ⋯)
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := (coreE₂CohomologicalFin l).i₃ r pq ⋯) (X₁ := (coreE₂CohomologicalFin l).i₃ r' pq ⋯)
        (homOfLE ⋯ : (coreE₂CohomologicalFin l).i₃ r pq ⋯ ⟶ (coreE₂CohomologicalFin l).i₃ r' pq ⋯)))

Tactic:
apply E.isZero_H_map_mk₁_of_isIso

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_2 : Y.IsFirstQuadrant
i j : EInt
hij : i ≤ j
hj : j ≤ WithBotTop.coe 0
n : ℤ
⊢ IsZero.{v_1, u_1} ((Y.H n).obj (mk₁ (homOfLE hij)))

Tactic:
IsFirstQuadrant.isZero₁ i j hij hj n

Premises used: CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_2 : Y.IsFirstQuadrant
i j : EInt
hij : i ≤ j
n : ℤ
hi : WithBotTop.coe n < i
⊢ IsZero.{v_1, u_1} ((Y.H n).obj (mk₁ (homOfLE hij)))

Tactic:
IsFirstQuadrant.isZero₂ i j hij n hi

Premises used: CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂
-- 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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
hj : coreE₂CohomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe 0
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂CohomologicalNat.deg (p, q) + 1)).obj
      (mk₁ (X₀ := coreE₂CohomologicalNat.i₀ (r + 1) (p, q) ⋯) (X₁ := coreE₂CohomologicalNat.i₀ r (p, q) ⋯)
        (homOfLE ⋯ : coreE₂CohomologicalNat.i₀ (r + 1) (p, q) ⋯ ⟶ coreE₂CohomologicalNat.i₀ r (p, q) ⋯)))

Tactic:
apply isZero₁_of_isFirstQuadrant

Premises used: CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant
-- 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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
hj : (↑q : ℤ) - r + 2 ≤ 0
⊢ coreE₂CohomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe 0

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

Premises used: WithBotTop.coe_le_coe, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
hj : ∀ (this : 0 < (↑q : ℤ) - r + 2), False
⊢ (↑q : ℤ) - r + 2 ≤ 0

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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑q : ℤ) - r + 2
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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
hj : ∀ (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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
left : (↑(p, q).1 : ℤ) + (r, 1 - r).1 = (↑(p', q').1 : ℤ)
right : (↑(p, q).2 : ℤ) + (r, 1 - r).2 = (↑(p', q').2 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
⊢ (↑(p, q).1 : ℤ) + (r, 1 - r).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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
⊢ (↑(p, q).2 : ℤ) + (r, 1 - r).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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : 0 < (↑q : ℤ) - r + 2
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.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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
hi : WithBotTop.coe (coreE₂CohomologicalNat.deg (p, q) - 1) < coreE₂CohomologicalNat.i₃ r (p, q) ⋯
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂CohomologicalNat.deg (p, q) - 1)).obj
      (mk₁ (X₀ := coreE₂CohomologicalNat.i₃ r (p, q) ⋯) (X₁ := coreE₂CohomologicalNat.i₃ (r + 1) (p, q) ⋯)
        (homOfLE ⋯ : coreE₂CohomologicalNat.i₃ r (p, q) ⋯ ⟶ coreE₂CohomologicalNat.i₃ (r + 1) (p, q) ⋯)))

Tactic:
apply isZero₂_of_isFirstQuadrant

Premises used: CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant
-- 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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
hi : HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 < (↑q : ℤ) + r - 1
⊢ WithBotTop.coe (coreE₂CohomologicalNat.deg (p, q) - 1) < coreE₂CohomologicalNat.i₃ r (p, q) ⋯

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

Premises used: CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg, WithBotTop.coe_lt_coe, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
hi : ∀ (this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1), False
⊢ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 < (↑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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
⊢ 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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
hi : ∀ (q' : ℕ) (hq' : HSub.hSub (α := ℤ) (↑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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : HSub.hSub (α := ℤ) (↑q : ℤ) 1 + r = (↑q' : ℤ)
left : (↑(p', q').1 : ℤ) + (r, 1 - r).1 = (↑(p, q).1 : ℤ)
right : (↑(p', q').2 : ℤ) + (r, 1 - r).2 = (↑(p, q).2 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : HSub.hSub (α := ℤ) (↑q : ℤ) 1 + r = (↑q' : ℤ)
⊢ (↑(p', q').1 : ℤ) + (r, 1 - r).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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : HSub.hSub (α := ℤ) (↑q : ℤ) 1 + r = (↑q' : ℤ)
⊢ (↑(p', q').2 : ℤ) + (r, 1 - r).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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : HSub.hSub (α := ℤ) (↑q : ℤ) 1 + r = (↑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
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_2 : Y.IsThirdQuadrant
i j : EInt
hij : i ≤ j
hi : WithBotTop.coe 0 < i
n : ℤ
⊢ IsZero.{v_1, u_1} ((Y.H n).obj (mk₁ (homOfLE hij)))

Tactic:
IsThirdQuadrant.isZero₁ i j hij hi n

Premises used: CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_2 : Y.IsThirdQuadrant
i j : EInt
hij : i ≤ j
n : ℤ
hj : j ≤ WithBotTop.coe n
⊢ IsZero.{v_1, u_1} ((Y.H n).obj (mk₁ (homOfLE hij)))

Tactic:
IsThirdQuadrant.isZero₂ i j hij n hj

Premises used: CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂