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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_15
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_16
⊢ (↑(Fin.clamp ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l) : ℕ) ≤
    (↑(Fin.clamp ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l) : ℕ)

Tactic:
exact Fin.clamp_monotone (by lia)

Premises used: Fin.clamp_monotone
-- 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
b : ℤ
b' : ℕ
isLt_1 : b' < l
h₁ : (a, (⟨a', isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b, (⟨b', isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_20
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_21
h :
  (↑(⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) : ℕ) =
    (↑(b, (⟨b', isLt_1⟩ : Fin l)).2.castSucc : ℕ)
⊢ (⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) =
    (b, (⟨b', isLt_1⟩ : Fin l)).2.castSucc

Tactic:
ext
-- 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
b : ℤ
b' : ℕ
isLt_1 : b' < l
h₁ : (a, (⟨a', isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b, (⟨b', isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_20
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_21
h : ((↑a' : ℤ) - (r' - 2)).toNat = b'
⊢ (↑(⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) : ℕ) =
    (↑(b, (⟨b', isLt_1⟩ : Fin l)).2.castSucc : ℕ)

Tactic:
dsimp
-- 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
b : ℤ
b' : ℕ
isLt_1 : b' < l
h₁ : (a, (⟨a', isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b, (⟨b', isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_20
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_21
⊢ ((↑a' : ℤ) - (r' - 2)).toNat = b'

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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
b : ℤ
b' : ℕ
isLt_1 : b' < l
h₁ : (a, (⟨a', isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b, (⟨b', isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_22
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_23
h :
  (↑(Fin.clamp ((↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l) : ℕ) =
    (↑(a, (⟨a', isLt⟩ : Fin l)).2.succ : ℕ)
⊢ Fin.clamp ((↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l = (a, (⟨a', isLt⟩ : Fin l)).2.succ

Tactic:
ext
-- 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
b : ℤ
b' : ℕ
isLt_1 : b' < l
h₁ : (a, (⟨a', isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b, (⟨b', isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_22
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_23
h : min ((↑b' : ℤ) + (r' - 1)).toNat l = a' + 1
⊢ (↑(Fin.clamp ((↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l) : ℕ) =
    (↑(a, (⟨a', isLt⟩ : Fin l)).2.succ : ℕ)

Tactic:
dsimp
-- 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
b : ℤ
b' : ℕ
isLt_1 : b' < l
h₁ : (a, (⟨a', isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b, (⟨b', isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_22
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_23
⊢ min ((↑b' : ℤ) + (r' - 1)).toNat l = a' + 1

Tactic:
grind
-- 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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
simp : -(↑pq.2 : ℤ) - r + 2 ≤ -(↑pq.2 : ℤ)
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r + 2) ≤ WithBotTop.coe (-(↑pq.2 : ℤ))

Tactic:
simp
-- 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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ -(↑pq.2 : ℤ) - r + 2 ≤ -(↑pq.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₀ : ℤ
pq : ℕ × ℕ
⊢ WithBotTop.coe (-(↑pq.2 : ℤ)) ≤ WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1)

Tactic:
simp
-- 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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
simp : HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1 ≤ -(↑pq.2 : ℤ) + r - 1
⊢ WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1) ≤ WithBotTop.coe (-(↑pq.2 : ℤ) + r - 1)

Tactic:
simp
-- 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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1 ≤ -(↑pq.2 : ℤ) + 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₀ r : ℤ
pq pq' : ℕ × ℕ
hpq : (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq pq'
hr : 2 ≤ r
⊢ (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)

Tactic:
simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq

Premises used: ComplexShape.spectralSequenceNat_rel_iff
-- 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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
⊢ HSub.hSub (α := ℤ) (-(↑pq.1 : ℤ)) (↑pq.2 : ℤ) + 1 = HSub.hSub (α := ℤ) (-(↑pq'.1 : ℤ)) (↑pq'.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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r + 2) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq'.2 : ℤ)) 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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe (-(↑pq.2 : ℤ)) = WithBotTop.coe (-(↑pq'.2 : ℤ) + 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₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' simp : r ≤ r'
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r' + 2) ≤ WithBotTop.coe (-(↑pq.2 : ℤ) - r + 2)

Tactic:
simp
-- 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₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' simp : r ≤ r'
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) + r - 1) ≤ WithBotTop.coe (-(↑pq.2 : ℤ) + r' - 1)

Tactic:
simp
-- 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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hpq : (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq pq'
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)

Tactic:
simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq

Premises used: ComplexShape.spectralSequenceNat_rel_iff
-- 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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r' + 2) = WithBotTop.coe (-(↑pq'.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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe (-(↑pq'.2 : ℤ) + r' - 1) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
⊢ IsZero.{v_1, u_1}
    ((X.H n).obj (mk₁ (X₀ := data.i₀ r' pq ⋯) (X₁ := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r' pq ⋯ ⟶ data.i₀ r pq ⋯)))

Tactic:
HasSpectralSequence.isZero_H_obj_mk₁_i₀_le r r' pq hpq n hn

Premises used: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq ⋯
hi₀ : i₀ = data.i₀ r pq ⋯
⊢ i₀' ≤ i₀

Tactic:
simpa only [hi₀', hi₀] using data.i₀_le r r' pq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq ⋯
hi₀ : i₀ = data.i₀ r pq ⋯
subst : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₀ r' pq ⋯) (X₁ := data.i₀ r pq ⋯) (homOfLE ⋯)))
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := i₀') (X₁ := i₀) (homOfLE ⋯)))

Tactic:
subst hi₀' hi₀
-- 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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₀ r' pq ⋯) (X₁ := data.i₀ r pq ⋯) (homOfLE ⋯)))

Tactic:
HasSpectralSequence.isZero_H_obj_mk₁_i₀_le r r' pq hpq n hn

Premises used: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₀ r' pq ⋯) (X₁ := data.i₀ r pq ⋯) (homOfLE ⋯)))

Tactic:
exact HasSpectralSequence.isZero_H_obj_mk₁_i₀_le r r' pq hpq n hn

Premises used: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
⊢ IsZero.{v_1, u_1}
    ((X.H n).obj (mk₁ (X₀ := data.i₃ r pq ⋯) (X₁ := data.i₃ r' pq ⋯) (homOfLE ⋯ : data.i₃ r pq ⋯ ⟶ data.i₃ r' pq ⋯)))

Tactic:
HasSpectralSequence.isZero_H_obj_mk₁_i₃_le r r' pq hpq n hn

Premises used: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq ⋯
hi₃' : i₃' = data.i₃ r' pq ⋯
⊢ i₃ ≤ i₃'

Tactic:
simpa only [hi₃, hi₃'] using data.i₃_le r r' pq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq ⋯
hi₃' : i₃' = data.i₃ r' pq ⋯
subst : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₃ r pq ⋯) (X₁ := data.i₃ r' pq ⋯) (homOfLE ⋯)))
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := i₃) (X₁ := i₃') (homOfLE ⋯)))

Tactic:
subst hi₃ hi₃'
-- 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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₃ r pq ⋯) (X₁ := data.i₃ r' pq ⋯) (homOfLE ⋯)))

Tactic:
HasSpectralSequence.isZero_H_obj_mk₁_i₃_le r r' pq hpq n hn

Premises used: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_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
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₃ r pq ⋯) (X₁ := data.i₃ r' pq ⋯) (homOfLE ⋯)))

Tactic:
exact HasSpectralSequence.isZero_H_obj_mk₁_i₃_le r r' pq hpq n hn

Premises used: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_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
E : SpectralObject.{u_1, 0, v_1, 0} C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = coreE₂Cohomological.deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
exfalso : False
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := coreE₂Cohomological.i₀ r' pq ⋯) (X₁ := coreE₂Cohomological.i₀ r pq ⋯)
        (homOfLE ⋯ : coreE₂Cohomological.i₀ r' pq ⋯ ⟶ coreE₂Cohomological.i₀ r pq ⋯)))

Tactic:
exfalso
-- 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
E : SpectralObject.{u_1, 0, v_1, 0} C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = coreE₂Cohomological.deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ False

Tactic:
hpq _ rfl

Premises used: rfl
-- 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
E : SpectralObject.{u_1, 0, v_1, 0} C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = coreE₂Cohomological.deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ False

Tactic:
exact hpq _ rfl

Premises used: rfl
-- 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
E : SpectralObject.{u_1, 0, v_1, 0} C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = coreE₂Cohomological.deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
exfalso : False
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := coreE₂Cohomological.i₃ r pq ⋯) (X₁ := coreE₂Cohomological.i₃ r' pq ⋯)
        (homOfLE ⋯ : coreE₂Cohomological.i₃ r pq ⋯ ⟶ coreE₂Cohomological.i₃ r' pq ⋯)))

Tactic:
exfalso
-- 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
E : SpectralObject.{u_1, 0, v_1, 0} C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = coreE₂Cohomological.deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (ComplexShape.up' (r, 1 - r)).Rel (pq - (r, 1 - r)) pq

Tactic:
simp
-- 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
E : SpectralObject.{u_1, 0, v_1, 0} C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = coreE₂Cohomological.deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ False

Tactic:
exact hpq (pq - (r, 1 - r)) (by simp)

Premises used: HSub.hSub, Prod.mk, OfNat.ofNat
-- 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
subst : (coreE₂CohomologicalFin l).i₀ (r + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯
⊢ (coreE₂CohomologicalFin l).i₀ r' pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯

Tactic:
subst hrr'
-- 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 : ℤ
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
hr : 2 ≤ r
obtain :
  ∀ (k : ℕ)
    (hpq :
      ∀ (pq' : ℤ × Fin l),
        ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel pq
            pq')
    (hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)),
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) pq ⋯ =
      (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) pq ⋯
⊢ (coreE₂CohomologicalFin l).i₀ (r + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯

Tactic:
obtain ⟨k, rfl⟩ := Int.le.dest hr

Premises used: Int.le.dest, rfl