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₀ : ℤ
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 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) (p', q')
have right : (↑(p, q).2 : ℤ) + (r, 1 - r).2 = (↑(p', q').2 : ℤ)
Tactic: constructor
-- 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
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
⊢ 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) ⋯)))
have hi : WithBotTop.coe (coreE₂CohomologicalNat.deg (p, q) - 1) < coreE₂CohomologicalNat.i₃ r (p, q) sorry
Tactic: apply isZero₂_of_isFirstQuadrant
-- 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
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
⊢ WithBotTop.coe (coreE₂CohomologicalNat.deg (p, q) - 1) < coreE₂CohomologicalNat.i₃ r (p, q) ⋯
have hi : HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 < (↑q : ℤ) + r - 1
Tactic: simp only [coreE₂CohomologicalNat_deg, coreE₂CohomologicalNat_i₃, WithBotTop.coe_lt_coe]
-- 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
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
⊢ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 < (↑q : ℤ) + r - 1
have hi : ∀ (this : (↑q : ℤ) + r - 1 ≤ HAdd.hAdd (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1), False
Tactic: by_contra!
-- 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
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
⊢ False
have hi : ∀ (p' : ℕ) (hp' : (↑p : ℤ) - r = (↑p' : ℤ)), False
Tactic: obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p - r by lia)
-- 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
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' : ℤ)
⊢ False
have hi : ∀ (q' : ℕ) (hq' : HSub.hSub (α := ℤ) (↑q : ℤ) 1 + r = (↑q' : ℤ)), False
Tactic: obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q - 1 + r by lia)
-- 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
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' : ℤ)
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p', q') (p, q)
have left : (↑(p', q').1 : ℤ) + (r, 1 - r).1 = (↑(p, q).1 : ℤ)
Tactic: constructor
-- 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
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 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p', q') (p, q)
have right : (↑(p', q').2 : ℤ) + (r, 1 - r).2 = (↑(p, q).2 : ℤ)
Tactic: constructor
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂HomologicalNat.deg (p, q) + 1)).obj
      (mk₁ (X₀ := coreE₂HomologicalNat.i₀ (r + 1) (p, q) ⋯) (X₁ := coreE₂HomologicalNat.i₀ r (p, q) ⋯)
        (homOfLE ⋯ : coreE₂HomologicalNat.i₀ (r + 1) (p, q) ⋯ ⟶ coreE₂HomologicalNat.i₀ r (p, q) ⋯)))
have hj : coreE₂HomologicalNat.i₀ r (p, q) sorry ≤ WithBotTop.coe (coreE₂HomologicalNat.deg (p, q) + 1)
Tactic: apply isZero₂_of_isThirdQuadrant
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
⊢ coreE₂HomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe (coreE₂HomologicalNat.deg (p, q) + 1)
have hj : -(↑q : ℤ) - r + 2 ≤ HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1
Tactic: simp only [coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_deg, WithBotTop.coe_le_coe]
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
⊢ -(↑q : ℤ) - r + 2 ≤ HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1
have hj : ∀ (this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2), False
Tactic: by_contra!
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
⊢ False
have hj : ∀ (p' : ℕ) (hp' : (↑p : ℤ) - r = (↑p' : ℤ)), False
Tactic: obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p - r by lia)
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
⊢ False
have hj : ∀ (q' : ℕ) (hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)), False
Tactic: obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + r - 1 by lia)
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) (p', q')
have left : (↑(p, q).1 : ℤ) + (-r, r - 1).1 = (↑(p', q').1 : ℤ)
Tactic: constructor
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
this : HSub.hSub (α := ℤ) (-(↑p : ℤ)) (↑q : ℤ) + 1 < -(↑q : ℤ) - r + 2
p' : ℕ
hp' : (↑p : ℤ) - r = (↑p' : ℤ)
q' : ℕ
hq' : (↑q : ℤ) + r - 1 = (↑q' : ℤ)
left : (↑(p, q).1 : ℤ) + (-r, r - 1).1 = (↑(p', q').1 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) (p', q')
have right : (↑(p, q).2 : ℤ) + (-r, r - 1).2 = (↑(p', q').2 : ℤ)
Tactic: constructor
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂HomologicalNat.deg (p, q) - 1)).obj
      (mk₁ (X₀ := coreE₂HomologicalNat.i₃ r (p, q) ⋯) (X₁ := coreE₂HomologicalNat.i₃ (r + 1) (p, q) ⋯)
        (homOfLE ⋯ : coreE₂HomologicalNat.i₃ r (p, q) ⋯ ⟶ coreE₂HomologicalNat.i₃ (r + 1) (p, q) ⋯)))
have hi : WithBotTop.coe 0 < coreE₂HomologicalNat.i₃ r (p, q) sorry
Tactic: apply isZero₁_of_isThirdQuadrant
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
⊢ WithBotTop.coe 0 < coreE₂HomologicalNat.i₃ r (p, q) ⋯
have hi : 0 < -(↑q : ℤ) + r - 1
Tactic: simp only [coreE₂HomologicalNat_i₃, WithBotTop.coe_lt_coe]
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
⊢ 0 < -(↑q : ℤ) + r - 1
have hi : ∀ (this : -(↑q : ℤ) + r - 1 ≤ 0), False
Tactic: by_contra!
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
⊢ False
have hi : ∀ (p' : ℕ) (hp' : (↑p : ℤ) + r = (↑p' : ℤ)), False
Tactic: obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p + r by lia)
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
⊢ False
have hi : ∀ (q' : ℕ) (hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)), False
Tactic: obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + 1 - r by lia)
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p', q') (p, q)
have left : (↑(p', q').1 : ℤ) + (-r, r - 1).1 = (↑(p, q).1 : ℤ)
Tactic: constructor
-- 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
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_4 : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_6
this : -(↑q : ℤ) + r - 1 ≤ 0
p' : ℕ
hp' : (↑p : ℤ) + r = (↑p' : ℤ)
q' : ℕ
hq' : HAdd.hAdd (α := ℤ) (↑q : ℤ) 1 - r = (↑q' : ℤ)
left : (↑(p', q').1 : ℤ) + (-r, r - 1).1 = (↑(p, q).1 : ℤ)
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p', q') (p, q)
have right : (↑(p', q').2 : ℤ) + (-r, r - 1).2 = (↑(p, q).2 : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ sorry sorry sorry).X₂),
  x₂ ≫ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ sorry sorry sorry).g = 0 →
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ sorry sorry sorry).X₁),
      π ≫ x₂ = x₁ ≫ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ sorry sorry sorry).f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₁),
    π ≫ x₂ = x₁ ≫ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f
have dsimp : ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry),
  π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ sorry sorry sorry
Tactic: dsimp at hx₂ ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
have hx₂' : CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry)
    (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ sorry sorry) (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry) =
  CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry) 0 (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry)
Tactic: have hx₂' := hx₂ =≫ X.ιE ..
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ :
  Eq (α := A ⟶ X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯)
    0
hx₂' :
  CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯)
      (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯) 0 (X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
have hx₂'₁ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ sorry sorry ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry = 0
Tactic: rw [assoc, zero_comp, X.map_ιE f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄)
    (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄) n₁ n₂ n₃] at hx₂'
Cleared hypotheses: hx₂'