awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃ = data.i₁ pq
have rw : data.i₃ r pq' sorry = data.i₁ pq
Tactic: rw [hi₃, data.hc₁₃ r _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
rw : data.i₃ r pq' ⋯ = data.i₁ pq
⊢ i₃ = data.i₁ pq
have rw₁ : data.i₃ r pq' sorry = data.i₃ r pq' sorry
Tactic: rw [hi₃, data.hc₁₃ r _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃' = data.i₂ pq
have rw : data.i₃ r' pq' sorry = data.i₂ pq
Tactic: rw [hi₃', data.i₃_next r r' _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
rw : data.i₃ r' pq' ⋯ = data.i₂ pq
⊢ i₃' = data.i₂ pq
have rw₁ : data.i₂ pq = data.i₂ pq
Tactic: rw [hi₃', data.i₃_next r r' _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ n₀ = data.deg pq
have this : data.deg pq + 1 = data.deg pq'
Tactic: have := data.hc r pq pq' h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ Eq (α := pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (pageD X data r pq pq' ⋯ ≫
        Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
          X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ :
      pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (0 : (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
have pos : Eq.{v_1 + 1} (α := pageX X data r pq sorry ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry) 0 0
Tactic: rw [pageD_eq X data r hr pq pq' h (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
      (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
      (homOfLE (data.le₃₃' hrr' hr pq' hi₃ hi₃'))
      (homOfLE (by simpa only [hi₃', data.i₃_next r r' _ _ h] using data.le₂₃ r pq))
      hi₀ hi₁ (by rw [hi₂, data.hc₀₂ r _ _ h])
      (by rw [hi₃, data.hc₁₃ r _ _ h]) (by rw [hi₃', data.i₃_next r r' _ _ h]) rfl
      (n₀ - 1) n₀ n₁ n₂ (by have := data.hc r pq pq' h; lia) (by simp) hn₁ hn₂,
      Category.assoc, Category.assoc, Iso.inv_hom_id_assoc,
      d_map_fourδ₄Toδ₃ .., comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq pq'
⊢ Eq (α := (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    ((page X data r hr).d pq pq' ≫
        Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
          X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ :
      (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (0 : (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
have neg : Eq (α := (page X data r hr).X pq ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
  (0 ≫
      Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' sorry sorry) ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' sorry sorry sorry sorry n₀ n₁ n₂ sorry sorry :
    (page X data r hr).X pq ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
  (0 : (page X data r hr).X pq ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
Tactic: rw [HomologicalComplex.shape _ _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq pq'
neg :
  Eq (α := (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (0 ≫
        Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
          X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ :
      (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (0 : (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
⊢ Eq (α := (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    ((page X data r hr).d pq pq' ≫
        Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
          X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ :
      (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (0 : (page X data r hr).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
have neg₁ : Eq.{v_1 + 1} (α := (page X data r hr).X pq ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry) 0 0
Tactic: rw [HomologicalComplex.shape _ _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).g
have dsimp : Epi (Y := X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
  (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' sorry sorry) ≫
      X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' sorry sorry sorry sorry n₀ n₁ n₂ sorry sorry :
    pageX X data r pq' sorry ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
h : ¬(c r).Rel pq pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯) (Y :=
    X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
have apply : IsZero.{v_1, u_1} ((X.H n₀).obj (mk₁ (homOfLE sorry)))
Tactic: apply X.isIso_map_fourδ₄Toδ₃_of_isZero _ _ _ _ _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
h : ¬(c r).Rel pq pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsZero.{v_1, u_1} ((X.H n₀).obj (mk₁ (homOfLE ⋯)))
have refine : ∀ (x : κ) (hk : (c r).Rel x pq'), False
Tactic: refine X.isZero_H_obj_mk₁_i₃_le' data r r' hrr' hr pq' (fun _ hk ↦ ?_) _ (by lia) _ _ hi₃ hi₃'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
h : ¬(c r).Rel pq pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
x : κ
hk : (c r).Rel x pq'
⊢ False
have hk₁ : (c r).Rel ((c r).prev pq') pq'
Tactic: obtain rfl := (c r).prev_eq' hk
Cleared hypotheses: x, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
h : ¬(c r).Rel pq pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hk : (c r).Rel ((c r).prev pq') pq'
⊢ False
have h₁ : ¬(c r).Rel ((c r).prev pq') pq'
Tactic: subst hpq
Cleared hypotheses: pq, hpq, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).Exact
have pos : ∀ (h : (c r).Rel pq pq'), (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' sorry sorry).Exact
Tactic: by_cases h : (c r).Rel pq pq'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
pos :
  ∀ (h : (c r).Rel pq pq'),
    (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).Exact
⊢ (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).Exact
have neg : ∀ (h : ¬(c r).Rel pq pq'),
  (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' sorry sorry).Exact
Tactic: by_cases h : (c r).Rel pq pq'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).Exact
have pos : ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' sorry sorry ≅
  X.dCokernelSequence (i₅ := data.i₃ r pq sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry)
    (have this : i₃' ⟶ data.i₃ r pq sorry := homOfLE sorry;
    this)
    (homOfLE sorry ≫ homOfLE sorry) sorry (n₀ - 1) n₀ n₁ n₂ sorry sorry sorry
Tactic: refine ShortComplex.exact_of_iso (Iso.symm ?_)
      (X.dCokernelSequence_exact
      (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
      (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
      (homOfLE (data.le₃₃' hrr' hr pq' hi₃ hi₃'))
      (show i₃' ⟶ data.i₃ r pq from homOfLE (by
        simpa only [hi₃', data.i₃_next r r' _ _ h] using data.le₂₃ r pq)) _ rfl
      (n₀ - 1) n₀ n₁ n₂ (by simp) hn₁ hn₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₂ = data.i₀ r pq ⋯
have rw : data.i₂ pq' = data.i₀ r pq sorry
Tactic: rw [hi₂, data.hc₀₂ r _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
rw : data.i₂ pq' = data.i₀ r pq ⋯
⊢ i₂ = data.i₀ r pq ⋯
have rw₁ : data.i₂ pq' = data.i₂ pq'
Tactic: rw [hi₂, data.hc₀₂ r _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃ = data.i₁ pq
have rw : data.i₃ r pq' sorry = data.i₁ pq
Tactic: rw [hi₃, data.hc₁₃ r _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
rw : data.i₃ r pq' ⋯ = data.i₁ pq
⊢ i₃ = data.i₁ pq
have rw₁ : data.i₃ r pq' sorry = data.i₃ r pq' sorry
Tactic: rw [hi₃, data.hc₁₃ r _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃' = data.i₂ pq
have rw : data.i₃ r' pq' sorry = data.i₂ pq
Tactic: rw [hi₃', data.i₃_next r r' _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
rw : data.i₃ r' pq' ⋯ = data.i₂ pq
⊢ i₃' = data.i₂ pq
have rw₁ : data.i₂ pq = data.i₂ pq
Tactic: rw [hi₃', data.i₃_next r r' _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (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 ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ n₀ = data.deg pq
have this : data.deg pq + 1 = data.deg pq'
Tactic: have := data.hc r _ _ h