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' : κ
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₁' ⋯ ⋯ ≅
    X.dCokernelSequence (i₅ := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
      (have this : i₃' ⟶ data.i₃ r pq ⋯ := homOfLE ⋯;
      this)
      (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯
have pos : Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq sorry) sorry sorry sorry sorry (n₀ - 1) n₀ n₁ sorry 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).f =
  (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).f ≫
    Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' sorry sorry)
Tactic: refine ShortComplex.isoMk
      (pageXIso X data _ hr _ _ _ _ _
        (by rw [hi₂, data.hc₀₂ r _ _ h]) (by rw [hi₃, data.hc₁₃ r _ _ h])
        (by rw [hi₃', data.i₃_next r r' _ _ h]) rfl _ _ _ (by have := data.hc r _ _ h; lia))
      (pageXIso X data _ hr _ _ _ _ _ hi₀ hi₁ hi₂ hi₃ _ _ _ hn₁') (Iso.refl _) ?_ (by simp)
-- 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'
⊢ Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) ≫
      (X.dCokernelSequence (i₅ := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
          (have this : i₃' ⟶ data.i₃ r pq ⋯ := homOfLE ⋯;
          this)
          (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯).f =
    (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).f ≫
      Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯)
have pos : Eq (α := pageX X data r pq sorry ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
  (CategoryStruct.comp (Y :=
    X.E (l := data.i₃ r pq sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : i₃' ⟶ data.i₃ r pq sorry) (n₀ - 1) n₀ n₁ sorry sorry)
    (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq sorry) sorry sorry sorry sorry (n₀ - 1) n₀ n₁ sorry sorry sorry) :
      pageX X data r pq sorry ⟶
        X.E (l := data.i₃ r pq sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : i₃' ⟶ data.i₃ r pq sorry) (n₀ - 1) n₀ n₁ sorry sorry)
    (X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (n₀ - 1) n₀ n₁ n₂ sorry sorry sorry :
      X.E (l := data.i₃ r pq sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry : i₃' ⟶ data.i₃ r pq sorry) (n₀ - 1) n₀ n₁ sorry sorry ⟶
        X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry))
  (pageD X data r pq pq' sorry ≫ Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' 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
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' 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' : κ
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' 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' : κ
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 neg : Mono (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).g
Tactic: refine (ShortComplex.exact_iff_mono _ ((page X data r hr).shape _ _ h)).mpr ?_
-- 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'
⊢ Mono (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).g
have this : IsIso (X := X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry) (Y :=
  X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
  (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' sorry sorry sorry sorry n₀ n₁ n₂ sorry sorry :
    X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
Tactic: have := isIso_mapFourδ₄Toδ₃' X data r r' hrr' hr pq pq' hpq
      i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' 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'
this :
  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₂ ⋯ ⋯)
⊢ Mono (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).g
have neg : Mono (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' 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₂
⊢ Fork.ι (kf X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
      Cofork.π (cc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯) =
    CategoryStruct.comp (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₂ ⋯ ⋯)
      (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 simp : Eq (α := X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry ⟶ X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
  (X.map (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry)
    (fourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ sorry sorry sorry sorry ≫ fourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' sorry sorry sorry sorry) n₀ n₁ n₂ sorry sorry)
  (X.map (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry)
    (CategoryStruct.comp (Y := mk₃ (homOfLE sorry) (homOfLE sorry) (homOfLE sorry))
      (fourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' sorry sorry sorry sorry :
        mk₃ (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) ⟶ mk₃ (homOfLE sorry) (homOfLE sorry) (homOfLE sorry))
      (fourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' sorry sorry sorry sorry :
        mk₃ (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) ⟶ mk₃ (homOfLE sorry) (homOfLE sorry) (homOfLE sorry)))
    n₀ n₁ n₂ sorry sorry)
Tactic: simp [← map_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₀
inst_3 : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequence_page_d_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_page_d_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) spectralSequence_page_d_eq._auto_3
⊢ i₂ = data.i₂ pq'
have rw : data.i₀ r pq sorry = data.i₂ pq'
Tactic: rw [h₂, ← 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₀
inst_3 : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequence_page_d_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_page_d_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) spectralSequence_page_d_eq._auto_3
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 [h₂, ← 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₀
inst_3 : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequence_page_d_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_page_d_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) spectralSequence_page_d_eq._auto_3
⊢ i₃ = data.i₃ r pq' ⋯
have rw : data.i₁ pq = data.i₃ r pq' sorry
Tactic: rw [h₃, 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₀
inst_3 : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequence_page_d_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_page_d_eq._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) spectralSequence_page_d_eq._auto_3
rw : data.i₁ pq = data.i₃ r pq' ⋯
⊢ i₃ = data.i₃ r pq' ⋯
have rw₁ : data.i₃ r pq' sorry = data.i₃ r pq' sorry
Tactic: rw [h₃, 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₀
inst_3 : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq : κ
n : ℤ
hn : n = data.deg pq
i₁ i₂ : ι
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ (homOfLE ⋯)))
⊢ IsZero.{v_1, u_1} (((X.spectralSequence data).page r ⋯).X pq)
have rw : IsZero.{v_1, u_1} (X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (n - 1) n (n + 1) sorry sorry)
Tactic: rw [X.isZero_spectralSequence_page_X_iff data r hr pq
    _ i₁ i₂ _ rfl h₁ h₂ rfl (n - 1) n (n + 1) 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₀
inst_3 : X.HasSpectralSequence data
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₂
⊢ Eq (α :=
    (((X.spectralSequence data).page r hr).sc' pq pq' pq'').homology ≅
      ShortComplex.RightHomologyData.H (S := ((X.spectralSequence data).page r hr).sc' pq pq' pq'')
        (ShortComplex.HomologyData.right
          (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂
            hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯)))
    (ShortComplex.RightHomologyData.homologyIso
      (ShortComplex.HomologyData.right
        (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
          hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯)))
    (ShortComplex.LeftHomologyData.homologyIso
      (ShortComplex.HomologyData.left
        (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
          hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯)))
have w : Eq (α :=
  (((X.spectralSequence data).page r hr).sc' pq pq' pq'').homology ⟶
    ShortComplex.RightHomologyData.H (S := ((X.spectralSequence data).page r hr).sc' pq pq' pq'')
      (ShortComplex.HomologyData.right
        (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
          hi₃' n₀ n₁ n₂ hn₁' sorry sorry)))
  (Iso.hom
    (ShortComplex.RightHomologyData.homologyIso
      (ShortComplex.HomologyData.right
        (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
          hi₃' n₀ n₁ n₂ hn₁' sorry sorry))))
  (Iso.hom
    (ShortComplex.LeftHomologyData.homologyIso
      (ShortComplex.HomologyData.left
        (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
          hi₃' n₀ n₁ n₂ hn₁' sorry sorry))))
Tactic: ext1
-- 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₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe 0
have simp : q + 1 ≤ 0
Tactic: simp
-- 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₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ IsZero.{v_1, u_1} ((Y.E₂SpectralSequence.page r ⋯).X (p, q))
have h : IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE sorry)))
Tactic: apply isZero_spectralSequence_page_X_of_isZero_H' _ _ _ hr
-- 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₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE ⋯)))
have h : WithBotTop.coe 0 < coreE₂Cohomological.i₁ (p, q)
Tactic: apply Y.isZero₁_of_isThirdQuadrant
-- 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₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ IsZero.{v_1, u_1} ((Y.E₂SpectralSequence.page r ⋯).X (p, q))
have h : IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE sorry)))
Tactic: apply isZero_spectralSequence_page_X_of_isZero_H' _ _ _ hr
-- 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₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ IsZero.{v_1, u_1} ((Y.H (coreE₂Cohomological.deg (p, q))).obj (mk₁ (X₀ := coreE₂Cohomological.i₁ (p, q)) (homOfLE ⋯)))
have h : coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe (coreE₂Cohomological.deg (p, q))
Tactic: apply Y.isZero₂_of_isThirdQuadrant
-- 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₀
Y : SpectralObject.{u_1, 0, v_1, 0} C EInt
inst_3 : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe (coreE₂Cohomological.deg (p, q))
have h : q + 1 ≤ p + q
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.Basic (goal)
Goal:
C : Type u_1
inst : Category.{u_3, u_1} C
inst_1 : Abelian.{u_3, u_1} C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E : SpectralSequence.{u_1, u_2, u_3} C c r₀
pq : κ
r r' : ℤ
h : r = r'
hr : r₀ ≤ r
⊢ (E.page r ⋯).X pq = (E.page r' ⋯).X pq
have subst : (E.page r sorry).X pq = (E.page r sorry).X pq
Tactic: subst h
Cleared hypotheses: r', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
u : ℤ × ℤ
i j j' : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i.fst : ℤ) + u.fst = (↑j'.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j'.snd : ℤ)
⊢ j = j'
have fst : j.fst = j'.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
u : ℤ × ℤ
i j j' : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i.fst : ℤ) + u.fst = (↑j'.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j'.snd : ℤ)
fst : j.fst = j'.fst
⊢ j = j'
have snd : j.snd = j'.snd
Tactic: ext