awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1) ≤ WithBotTop.coe ((↑pq.2 : ℤ) + r - 1)
have simp : HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1 ≤ (↑pq.2 : ℤ) + r - 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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, 1 - r)).Rel pq pq'
hr : 2 ≤ r
⊢ HAdd.hAdd (α := ℤ) (↑pq.1 : ℤ) (↑pq.2 : ℤ) + 1 = HAdd.hAdd (α := ℤ) (↑pq'.1 : ℤ) (↑pq'.2 : ℤ)
have hpq₁ : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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, 1 - r)).Rel pq pq'
hr : 2 ≤ r
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r + 2) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq'.2 : ℤ) 1)
have hpq₁ : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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, 1 - r)).Rel pq pq'
hr : 2 ≤ r
⊢ WithBotTop.coe (↑pq.2 : ℤ) = WithBotTop.coe ((↑pq'.2 : ℤ) + r - 1)
have hpq₁ : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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, 1 - r)).Rel pq pq'
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r' + 2) = WithBotTop.coe (↑pq'.2 : ℤ)
have hpq₁ : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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, 1 - r)).Rel pq pq'
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ WithBotTop.coe ((↑pq'.2 : ℤ) + r' - 1) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1)
have hpq₁ : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 p : ℤ
q : ℕ
hq : q < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_3
⊢ (⟨((↑(↑(p, (⟨q, hq⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat, ⋯⟩ : Fin (l + 1)) ≤ (p, (⟨q, hq⟩ : Fin l)).2.castSucc
have simp : (↑q : ℤ) - (r - 2) ≤ (↑q : ℤ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 : ℤ
pq : ℤ × Fin l
hr : 2 ≤ r
⊢ pq.2.succ ≤ Fin.clamp ((↑(↑pq.2 : ℕ) : ℤ) + (r - 1)).toNat l
have simp : (↑pq.2 : ℕ) + 1 ≤ ((↑(↑pq.2 : ℕ) : ℤ) + (r - 1)).toNat ∧ (↑pq.2 : ℕ) + 1 ≤ l
Tactic: simp only [Fin.le_iff_val_le_val, Fin.val_succ, le_min_iff, Fin.clamp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 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 : ℕ) : ℤ)
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_9
⊢ (a₁, (⟨a₂, isLt⟩ : Fin l)).2.castSucc = Fin.clamp ((↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l
have rw : (↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2.castSucc : ℕ) =
  (↑(Fin.clamp ((↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l) : ℕ)
Tactic: rw [Fin.ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 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 : ℕ) : ℤ)
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_9
⊢ (↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2.castSucc : ℕ) =
    (↑(Fin.clamp ((↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l) : ℕ)
have dsimp : a₂ = min ((↑b₂ : ℤ) + (r - 1)).toNat l
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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_11
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_12
⊢ (⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) ≤
    ⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat, ⋯⟩
have rw : ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat ≤
  ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat
Tactic: rw [Fin.mk_le_mk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) =
    (b, (⟨b', isLt_1⟩ : Fin l)).2.castSucc
have h : (↑(⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, sorry⟩ : Fin (l + 1)) : ℕ) =
  (↑(b, (⟨b', isLt_1⟩ : Fin l)).2.castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) : ℕ) =
    (↑(b, (⟨b', isLt_1⟩ : Fin l)).2.castSucc : ℕ)
have h : ((↑a' : ℤ) - (r' - 2)).toNat = b'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ Fin.clamp ((↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l = (a, (⟨a', isLt⟩ : Fin l)).2.succ
have h : (↑(Fin.clamp ((↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l) : ℕ) =
  (↑(a, (⟨a', isLt⟩ : Fin l)).2.succ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ (↑(Fin.clamp ((↑(↑(b, (⟨b', isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat l) : ℕ) =
    (↑(a, (⟨a', isLt⟩ : Fin l)).2.succ : ℕ)
have h : min ((↑b' : ℤ) + (r' - 1)).toNat l = a' + 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r + 2) ≤ WithBotTop.coe (-(↑pq.2 : ℤ))
have simp : -(↑pq.2 : ℤ) - r + 2 ≤ -(↑pq.2 : ℤ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1) ≤ WithBotTop.coe (-(↑pq.2 : ℤ) + r - 1)
have simp : HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1 ≤ -(↑pq.2 : ℤ) + r - 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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
⊢ HSub.hSub (α := ℤ) (-(↑pq.1 : ℤ)) (↑pq.2 : ℤ) + 1 = HSub.hSub (α := ℤ) (-(↑pq'.1 : ℤ)) (↑pq'.2 : ℤ)
have hpq₁ : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r + 2) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq'.2 : ℤ)) 1)
have hpq₁ : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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
⊢ WithBotTop.coe (-(↑pq.2 : ℤ)) = WithBotTop.coe (-(↑pq'.2 : ℤ) + r - 1)
have hpq₁ : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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
⊢ WithBotTop.coe (-(↑pq.2 : ℤ) - r' + 2) = WithBotTop.coe (-(↑pq'.2 : ℤ))
have hpq₁ : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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
⊢ WithBotTop.coe (-(↑pq'.2 : ℤ) + r' - 1) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1)
have hpq₁ : (↑pq.1 : ℤ) + -r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (r - 1) = (↑pq'.2 : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 ⋯
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := i₀') (X₁ := i₀) (homOfLE ⋯)))
have subst : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₀ r' pq sorry) (X₁ := data.i₀ r pq sorry) (homOfLE sorry)))
Tactic: subst hi₀' hi₀
Cleared hypotheses: i₀', i₀, hi₀', hi₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 ⋯
⊢ IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := i₃) (X₁ := i₃') (homOfLE ⋯)))
have subst : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (X₀ := data.i₃ r pq sorry) (X₁ := data.i₃ r' pq sorry) (homOfLE sorry)))
Tactic: subst hi₃ hi₃'
Cleared hypotheses: i₃, i₃', hi₃, hi₃'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ 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 ⋯)))
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ 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 ⋯)))
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 ⋯
have subst : (coreE₂CohomologicalFin l).i₀ (r + 1) pq sorry = (coreE₂CohomologicalFin l).i₀ r pq sorry
Tactic: subst hrr'
Cleared hypotheses: r', hrr'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
⊢ (coreE₂CohomologicalFin l).i₀ (r + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯
have 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 sorry =
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) pq sorry
Tactic: obtain ⟨k, rfl⟩ := Int.le.dest hr
Cleared hypotheses: r, hpq, hr
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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 : ℤ)
⊢ (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) pq ⋯ =
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) pq ⋯
have 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)) sorry =
    (coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, ⟨q, hq⟩) sorry
Tactic: obtain ⟨p, q, hq⟩ := pq
Cleared hypotheses: pq, hn, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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'
⊢ (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⟩) ⋯
have h : (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) sorry) : ℕ) =
  (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, (⟨q, hq⟩ : Fin l)) sorry) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
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
have by_contra! : ∀ (this : k < q), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
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
⊢ False
have hpq₁ : ∀ (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
Cleared hypotheses: hpq