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))
pq : ℤ × Fin l
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
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 : ℤ)
obtain :
  ∀ (p : ℤ) (q : ℕ) (hq : q < l) (hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1)
    (hpq :
      ∀ (pq' : ℤ × Fin l),
        ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel
            (p, ⟨q, hq⟩) pq'),
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) ⋯ =
      (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, ⟨q, hq⟩) ⋯
⊢ (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) pq ⋯ =
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) pq ⋯

Tactic:
obtain ⟨p, q, hq⟩ := pq
-- 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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
hpq :
  ∀ (pq' : ℤ × Fin l),
    ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel
        (p, ⟨q, hq⟩) pq'
h :
  (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ) =
    (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ)
⊢ (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) ⋯ =
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, ⟨q, hq⟩) ⋯

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₀ : ℤ
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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
hpq :
  ∀ (pq' : ℤ × Fin l),
    ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel
        (p, ⟨q, hq⟩) pq'
by_contra! : ∀ (this : k < q), False
⊢ q ≤ k

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

Tactic:
simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq

Premises used: ComplexShape.spectralSequenceFin_rel_iff, Prod.forall, not_and
-- 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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
this : k < q
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑q : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
obtain :
  ∀ (t : ℕ) (hq : k + 1 + t < l) (hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1)
    (this : k < k + 1 + t)
    (hpq :
      ∀ (a : ℤ) (b : Fin l),
        p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a →
          ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)),
    False
⊢ False

Tactic:
obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)

Premises used: Nat.add_one_le_of_lt, Nat.le.dest, 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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1
this : k < k + 1 + t
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
⊢ t < l

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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1
this : k < k + 1 + t
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
simp : HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + (↑t : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑t : ℤ)
⊢ (↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑(⟨t, ⋯⟩ : Fin l) : ℕ) : ℤ)

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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1
this : k < k + 1 + t
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + (↑t : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑t : ℤ)

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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1
this : k < k + 1 + t
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
⊢ False

Tactic:
exact hpq _ ⟨t, by lia⟩ rfl (by simp; lia)

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

Tactic:
have h : q ≤ k := by
        by_contra!
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)
        exact hpq _ ⟨t, by lia⟩ rfl (by simp; 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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
hpq :
  ∀ (pq' : ℤ × Fin l),
    ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel
        (p, ⟨q, hq⟩) pq'
h : q ≤ k
h₁ :
  ∀ (hn : n = p + (↑q : ℤ) + 1)
    (hpq :
      ∀ (a : ℤ) (b : Fin l),
        p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑q : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ))
    (h : q ≤ k), (↑q : ℤ) - (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1 - 2) ≤ 0
⊢ (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ) =
    (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ)

Tactic:
simp_all
-- 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))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = p + (↑q : ℤ) + 1
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑q : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
h : q ≤ k
⊢ (↑q : ℤ) - (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1 - 2) ≤ 0

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 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 ⟨k, rfl⟩ := Int.le.dest hr
      obtain ⟨p, q, hq⟩ := pq
      ext
      have h : q ≤ k := by
        by_contra!
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)
        exact hpq _ ⟨t, by lia⟩ rfl (by simp; lia)
      simp_all
      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
ι : 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 pq ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) 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 :
  ∀ (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),
    (coreE₂CohomologicalFin l).i₃ r (p, (⟨q, hq⟩ : Fin l)) ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) ⋯
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) pq ⋯

Tactic:
obtain ⟨p, q, hq⟩ := pq
-- 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
by_contra! : ∀ (this : (↑q : ℤ) + r ≤ (↑l : ℤ)), False
⊢ (↑l : ℤ) < (↑q : ℤ) + r

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
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
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
obtain : ∀ (t : ℕ) (ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)), False
⊢ False

Tactic:
obtain ⟨t, ht⟩ := Int.le.dest this

Premises used: Int.le.dest
-- 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
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
t : ℕ
ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)
⊢ ∀ (a : ℤ) (b : Fin l), a + r = p → ¬(↑(↑b : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)

Tactic:
simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq

Premises used: ComplexShape.spectralSequenceFin_rel_iff, Prod.forall, not_and
-- 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
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
t : ℕ
ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬(↑(↑b : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)
⊢ l - 1 - t < l

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
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
t : ℕ
ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬(↑(↑b : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)
⊢ p - r + r = p

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
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
t : ℕ
ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬(↑(↑b : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)
⊢ (↑(↑(⟨l - 1 - t, ⋯⟩ : Fin l) : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)

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
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
t : ℕ
ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬(↑(↑b : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)
⊢ False

Tactic:
exact hpq (p - r) ⟨l - 1 - t, by lia⟩ (by lia) (by lia)

Premises used: HSub.hSub, Fin.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 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
⊢ (↑l : ℤ) < (↑q : ℤ) + r

Tactic:
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)
-- 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
dsimp : Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + (r + 1 - 1)).toNat l
⊢ (coreE₂CohomologicalFin l).i₃ r (p, (⟨q, hq⟩ : Fin l)) ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) ⋯

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₀ : ℤ
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 - 1)).toNat

Tactic:
lia