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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
have pos : ∀ (hpq' : (c r).Rel pq' pq''), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
Tactic: by_cases hpq' : (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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
pos : ∀ (hpq' : (c r).Rel pq' pq''), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
have neg : ∀ (hpq' : ¬(c r).Rel pq' pq''), pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
Tactic: by_cases hpq' : (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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
have neg : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
  (CategoryStruct.comp (Y := pageX X data r pq' hr)
    (if hpq : (c r).Rel pq pq' then
      X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1)
          (data.deg pq + 2) sorry sorry sorry ≫
        (pageXIso X data r hr pq' (data.i₀ r pq' sorry) (data.i₁ pq') (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) sorry sorry sorry).inv
    else 0)
    (if hpq : (c r).Rel pq' pq'' then
      X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq' - 1) (data.deg pq')
          (data.deg pq' + 1) (data.deg pq' + 2) sorry sorry sorry ≫
        (pageXIso X data r hr pq'' (data.i₀ r pq'' sorry) (data.i₁ pq'') (data.i₀ r pq' sorry) (data.i₁ pq') sorry sorry sorry sorry
            (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) sorry sorry sorry).inv
    else 0))
  0
Tactic: dsimp only [pageD]
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
⊢ Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
have neg : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
  (CategoryStruct.comp (Y := pageX X data r pq' hr)
    (if hpq : (c r).Rel pq pq' then
      X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1)
          (data.deg pq + 2) sorry sorry sorry ≫
        (pageXIso X data r hr pq' (data.i₀ r pq' sorry) (data.i₁ pq') (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) sorry sorry sorry).inv
    else 0)
    0)
  0
Tactic: rw [dif_neg hpq', 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
neg :
  Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      0)
    0
⊢ Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
have neg₁ : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr) 0 0
Tactic: rw [dif_neg hpq', 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : ¬(c r).Rel pq pq'
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
have neg : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
  (CategoryStruct.comp (Y := pageX X data r pq' hr)
    (if hpq : (c r).Rel pq pq' then
      X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1)
          (data.deg pq + 2) sorry sorry sorry ≫
        (pageXIso X data r hr pq' (data.i₀ r pq' sorry) (data.i₁ pq') (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) sorry sorry sorry).inv
    else 0)
    (if hpq : (c r).Rel pq' pq'' then
      X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq' - 1) (data.deg pq')
          (data.deg pq' + 1) (data.deg pq' + 2) sorry sorry sorry ≫
        (pageXIso X data r hr pq'' (data.i₀ r pq'' sorry) (data.i₁ pq'') (data.i₀ r pq' sorry) (data.i₁ pq') sorry sorry sorry sorry
            (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) sorry sorry sorry).inv
    else 0))
  0
Tactic: dsimp only [pageD]
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : ¬(c r).Rel pq pq'
⊢ Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
have neg : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
  (CategoryStruct.comp (Y := pageX X data r pq' hr) 0
    (if hpq : (c r).Rel pq' pq'' then
      X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq' - 1) (data.deg pq')
          (data.deg pq' + 1) (data.deg pq' + 2) sorry sorry sorry ≫
        (pageXIso X data r hr pq'' (data.i₀ r pq'' sorry) (data.i₁ pq'') (data.i₀ r pq' sorry) (data.i₁ pq') sorry sorry sorry sorry
            (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) sorry sorry sorry).inv
    else 0))
  0
Tactic: rw [dif_neg hpq, 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : ¬(c r).Rel pq pq'
neg :
  Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr) 0
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
⊢ Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0)
      (if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0))
    0
have neg₁ : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr) 0 0
Tactic: rw [dif_neg hpq, zero_comp]
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ n₁ = data.deg pq
have this : data.deg pq + 1 = data.deg pq'
Tactic: have := data.hc r pq pq' hpq
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.i₂ pq'' = data.i₀ r pq' ⋯
have rw : data.i₂ pq'' = data.i₂ pq''
Tactic: rw [data.hc₀₂ r pq' pq'' hpq']
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.i₃ r pq'' ⋯ = data.i₁ pq'
have rw : data.i₃ r pq'' sorry = data.i₃ r pq'' sorry
Tactic: rw [data.hc₁₃ r pq' pq'' hpq']
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.i₀ r pq ⋯ = data.i₂ pq'
have rw : data.i₂ pq' = data.i₂ pq'
Tactic: rw [data.hc₀₂ r pq pq' hpq]
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ data.i₁ pq = data.i₃ r pq' ⋯
have rw : data.i₃ r pq' sorry = data.i₃ r pq' sorry
Tactic: rw [data.hc₁₃ r pq pq' hpq]
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ n₃ = data.deg pq''
have this : data.deg pq' + 1 = data.deg pq''
Tactic: have := data.hc r pq' pq'' hpq'
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ (page X data r hr).sc' pq pq' pq'' ≅
    X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
      (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂ n₃
      n₄ hn₁ hn₂ hn₃ hn₄
have refine_1 : Iso.hom (pageXIso X data r hr pq (data.i₀ r pq sorry) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq sorry) sorry sorry sorry sorry n₀ n₁ n₂ sorry sorry sorry) ≫
    (X.dShortComplex (i₀ := data.i₀ r pq'' sorry) (i₇ := data.i₃ r pq sorry) (homOfLE sorry : data.i₀ r pq'' sorry ⟶ data.i₁ pq'')
        (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : data.i₂ pq ⟶ data.i₃ r pq sorry) n₀ n₁ n₂
        n₃ n₄ hn₁ hn₂ hn₃ hn₄).f =
  ((page X data r hr).sc' pq pq' pq'').f ≫
    Iso.hom
      (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' sorry) (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry n₁ n₂ n₃ hn₂' sorry
        sorry)
Tactic: refine ShortComplex.isoMk
    (pageXIso _ _ _ hr _ _ _ _ _ rfl rfl rfl rfl _ _ _ (by have := data.hc r pq pq' hpq; lia))
    (pageXIso _ _ _ hr _ _ _ _ _ (by rw [data.hc₀₂ r pq' pq'' hpq'])
    (by rw [data.hc₁₃ r pq' pq'' hpq'])
    (by rw [data.hc₀₂ r pq pq' hpq]) (by rw [data.hc₁₃ r pq pq' hpq]) _ _ _ hn₂')
    (pageXIso _ _ _ hr _ _ _ _ _ rfl rfl rfl rfl _ _ _ (by have := data.hc r pq' pq'' hpq'; lia))
    ?_ ?_
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
refine_1 :
  Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).f =
    ((page X data r hr).sc' pq pq' pq'').f ≫
      Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯)
⊢ (page X data r hr).sc' pq pq' pq'' ≅
    X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
      (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂ n₃
      n₄ hn₁ hn₂ hn₃ hn₄
have refine_2 : Iso.hom
      (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' sorry) (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry n₁ n₂ n₃ hn₂' sorry
        sorry) ≫
    (X.dShortComplex (i₀ := data.i₀ r pq'' sorry) (i₇ := data.i₃ r pq sorry) (homOfLE sorry : data.i₀ r pq'' sorry ⟶ data.i₁ pq'')
        (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : data.i₂ pq ⟶ data.i₃ r pq sorry) n₀ n₁ n₂
        n₃ n₄ hn₁ hn₂ hn₃ hn₄).g =
  ((page X data r hr).sc' pq pq' pq'').g ≫
    Iso.hom
      (pageXIso X data r hr pq'' (data.i₀ r pq'' sorry) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' sorry) sorry sorry sorry sorry n₂ n₃ n₄ sorry
        sorry sorry)
Tactic: refine ShortComplex.isoMk
    (pageXIso _ _ _ hr _ _ _ _ _ rfl rfl rfl rfl _ _ _ (by have := data.hc r pq pq' hpq; lia))
    (pageXIso _ _ _ hr _ _ _ _ _ (by rw [data.hc₀₂ r pq' pq'' hpq'])
    (by rw [data.hc₁₃ r pq' pq'' hpq'])
    (by rw [data.hc₀₂ r pq pq' hpq]) (by rw [data.hc₁₃ r pq pq' hpq]) _ _ _ hn₂')
    (pageXIso _ _ _ hr _ _ _ _ _ rfl rfl rfl rfl _ _ _ (by have := data.hc r pq' pq'' hpq'; lia))
    ?_ ?_
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).f =
    ((page X data r hr).sc' pq pq' pq'').f ≫
      Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯)
have refine_1 : Iso.hom (pageXIso X data r hr pq (data.i₀ r pq sorry) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq sorry) sorry sorry sorry sorry n₀ n₁ n₂ sorry sorry sorry) ≫
    (X.dShortComplex (i₀ := data.i₀ r pq'' sorry) (i₇ := data.i₃ r pq sorry) (homOfLE sorry : data.i₀ r pq'' sorry ⟶ data.i₁ pq'')
          (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : data.i₂ pq ⟶ data.i₃ r pq sorry) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).f ≫
      Iso.inv
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' sorry) (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry n₁ n₂ n₃ hn₂'
          sorry sorry) =
  ((page X data r hr).sc' pq pq' pq'').f
Tactic: simp only [← Iso.comp_inv_eq, Category.assoc]
-- 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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
⊢ Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).g =
    ((page X data r hr).sc' pq pq' pq'').g ≫
      Iso.hom
        (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃ n₄
          ⋯ ⋯ ⋯)
have refine_2 : Iso.hom
      (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' sorry) (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry n₁ n₂ n₃ hn₂' sorry
        sorry) ≫
    (X.dShortComplex (i₀ := data.i₀ r pq'' sorry) (i₇ := data.i₃ r pq sorry) (homOfLE sorry : data.i₀ r pq'' sorry ⟶ data.i₁ pq'')
          (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : data.i₂ pq ⟶ data.i₃ r pq sorry) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).g ≫
      Iso.inv
        (pageXIso X data r hr pq'' (data.i₀ r pq'' sorry) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' sorry) sorry sorry sorry sorry n₂ n₃ n₄
          sorry sorry sorry) =
  ((page X data r hr).sc' pq pq' pq'').g
Tactic: simp only [← Iso.comp_inv_eq, Category.assoc]