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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
this : k < q
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑q : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
⊢ False
have obtain : ∀ (t : ℕ) (hq : k + 1 + t < l) (hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1)
  (this : k < k + 1 + t)
  (hpq :
    ∀ (a : ℤ) (b : Fin l),
      p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a →
        ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)),
  False
Tactic: obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)
Cleared hypotheses: q, hq, hn, this, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨k + 1 + t, hq⟩ : Fin l)) + 1
this : k < k + 1 + t
hpq :
  ∀ (a : ℤ) (b : Fin l),
    p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ)
⊢ (↑(k + 1 + t) : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑(⟨t, ⋯⟩ : Fin l) : ℕ) : ℤ)
have simp : HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + (↑t : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑t : ℤ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
hpq :
  ∀ (pq' : ℤ × Fin l),
    ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel
        (p, ⟨q, hq⟩) pq'
⊢ (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ) =
    (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ)
have h : q ≤ k
Tactic: have h : q ≤ k := by
        by_contra!
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)
        exact hpq _ ⟨t, by lia⟩ rfl (by simp; 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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) + 1
hpq :
  ∀ (pq' : ℤ × Fin l),
    ¬(ComplexShape.spectralSequenceFin l (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ), 1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ))).Rel
        (p, ⟨q, hq⟩) pq'
h : q ≤ k
⊢ (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ) =
    (↑((coreE₂CohomologicalFin l).i₀ (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) (p, (⟨q, hq⟩ : Fin l)) ⋯) : ℕ)
have h₁ : ∀ (hn : n = p + (↑q : ℤ) + 1)
  (hpq :
    ∀ (a : ℤ) (b : Fin l),
      p + HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) = a → ¬(↑q : ℤ) + (1 - HAdd.hAdd (α := ℤ) 2 (↑k : ℤ)) = (↑(↑b : ℕ) : ℤ))
  (h : q ≤ k), (↑q : ℤ) - (HAdd.hAdd (α := ℤ) 2 (↑k : ℤ) + 1 - 2) ≤ 0
Tactic: simp_all
Cleared hypotheses: hn, hpq, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := (coreE₂CohomologicalFin l).i₀ r' pq ⋯) (X₁ := (coreE₂CohomologicalFin l).i₀ r pq ⋯)
        (homOfLE ⋯ : (coreE₂CohomologicalFin l).i₀ r' pq ⋯ ⟶ (coreE₂CohomologicalFin l).i₀ r pq ⋯)))
have this : (coreE₂CohomologicalFin l).i₀ r' pq sorry = (coreE₂CohomologicalFin l).i₀ r pq sorry
Tactic: have : (coreE₂CohomologicalFin l).i₀ r' pq =
        (coreE₂CohomologicalFin l).i₀ r pq := by
      subst hrr'
      obtain ⟨k, rfl⟩ := Int.le.dest hr
      obtain ⟨p, q, hq⟩ := pq
      ext
      have h : q ≤ k := by
        by_contra!
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)
        exact hpq _ ⟨t, by lia⟩ rfl (by simp; lia)
      simp_all
      lia
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
this : (coreE₂CohomologicalFin l).i₀ r' pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := (coreE₂CohomologicalFin l).i₀ r' pq ⋯) (X₁ := (coreE₂CohomologicalFin l).i₀ r pq ⋯)
        (homOfLE ⋯ : (coreE₂CohomologicalFin l).i₀ r' pq ⋯ ⟶ (coreE₂CohomologicalFin l).i₀ r pq ⋯)))
have this₁ : IsIso (homOfLE sorry)
Tactic: have := isIso_homOfLE this
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ r' pq ⋯
have subst : (coreE₂CohomologicalFin l).i₃ r pq sorry = (coreE₂CohomologicalFin l).i₃ (r + 1) pq sorry
Tactic: subst hrr'
Cleared hypotheses: r', hrr'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) pq ⋯
have obtain : ∀ (p : ℤ) (q : ℕ) (hq : q < l)
  (hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩))
  (hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1),
  (coreE₂CohomologicalFin l).i₃ r (p, (⟨q, hq⟩ : Fin l)) sorry = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) sorry
Tactic: obtain ⟨p, q, hq⟩ := pq
Cleared hypotheses: pq, hpq, hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
⊢ (↑l : ℤ) < (↑q : ℤ) + r
have by_contra! : ∀ (this : (↑q : ℤ) + r ≤ (↑l : ℤ)), 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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
⊢ False
have obtain : ∀ (t : ℕ) (ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)), False
Tactic: obtain ⟨t, ht⟩ := Int.le.dest this
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
this : (↑q : ℤ) + r ≤ (↑l : ℤ)
t : ℕ
ht : (↑q : ℤ) + r + (↑t : ℤ) = (↑l : ℤ)
⊢ False
have hpq₁ : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬(↑(↑b : ℕ) : ℤ) + (1 - r) = (↑q : ℤ)
Tactic: simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
⊢ (coreE₂CohomologicalFin l).i₃ r (p, (⟨q, hq⟩ : Fin l)) ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) ⋯
have h : (↑l : ℤ) < (↑q : ℤ) + r
Tactic: have h : l < q + r := by
        by_contra!
        obtain ⟨t, ht⟩ := Int.le.dest this
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        exact hpq (p - r) ⟨l - 1 - t, by lia⟩ (by lia) (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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
h : (↑l : ℤ) < (↑q : ℤ) + r
⊢ (coreE₂CohomologicalFin l).i₃ r (p, (⟨q, hq⟩ : Fin l)) ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) ⋯
have dsimp : Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + (r + 1 - 1)).toNat l
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
h : (↑l : ℤ) < (↑q : ℤ) + r
⊢ Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + (r + 1 - 1)).toNat l
have rw : Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + r).toNat l
Tactic: rw [add_sub_cancel_right, Fin.clamp_eq_last _ _ (by lia), Fin.clamp_eq_last _ _ (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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
h : (↑l : ℤ) < (↑q : ℤ) + r
rw : Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + r).toNat l
⊢ Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + (r + 1 - 1)).toNat l
have rw₁ : Fin.last l = Fin.clamp ((↑q : ℤ) + r).toNat l
Tactic: rw [add_sub_cancel_right, Fin.clamp_eq_last _ _ (by lia), Fin.clamp_eq_last _ _ (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
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, (⟨q, hq⟩ : Fin l)) - 1
h : (↑l : ℤ) < (↑q : ℤ) + r
rw : Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + r).toNat l
rw₁ : Fin.last l = Fin.clamp ((↑q : ℤ) + r).toNat l
⊢ Fin.clamp ((↑q : ℤ) + (r - 1)).toNat l = Fin.clamp ((↑q : ℤ) + (r + 1 - 1)).toNat l
have rw₂ : Fin.last l = Fin.last l
Tactic: rw [add_sub_cancel_right, Fin.clamp_eq_last _ _ (by lia), Fin.clamp_eq_last _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := (coreE₂CohomologicalFin l).i₃ r pq ⋯) (X₁ := (coreE₂CohomologicalFin l).i₃ r' pq ⋯)
        (homOfLE ⋯ : (coreE₂CohomologicalFin l).i₃ r pq ⋯ ⟶ (coreE₂CohomologicalFin l).i₃ r' pq ⋯)))
have this : (coreE₂CohomologicalFin l).i₃ r pq sorry = (coreE₂CohomologicalFin l).i₃ r' pq sorry
Tactic: have : (coreE₂CohomologicalFin l).i₃ r pq = (coreE₂CohomologicalFin l).i₃ r' pq := by
      subst hrr'
      obtain ⟨p, q, hq⟩ := pq
      have h : l < q + r := by
        by_contra!
        obtain ⟨t, ht⟩ := Int.le.dest this
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        exact hpq (p - r) ⟨l - 1 - t, by lia⟩ (by lia) (by lia)
      dsimp
      rw [add_sub_cancel_right, Fin.clamp_eq_last _ _ (by lia), Fin.clamp_eq_last _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
data : SpectralSequenceDataCore ι c r₀
inst_3 : X.HasSpectralSequence data
l : ℕ
E : SpectralObject.{u_1, 0, v_1, 0} C (Fin (l + 1))
r r' : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
this : (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ r' pq ⋯
⊢ IsZero.{v_1, u_1}
    ((E.H n).obj
      (mk₁ (X₀ := (coreE₂CohomologicalFin l).i₃ r pq ⋯) (X₁ := (coreE₂CohomologicalFin l).i₃ r' pq ⋯)
        (homOfLE ⋯ : (coreE₂CohomologicalFin l).i₃ r pq ⋯ ⟶ (coreE₂CohomologicalFin l).i₃ r' pq ⋯)))
have this₁ : IsIso (homOfLE sorry)
Tactic: have := isIso_homOfLE this
-- 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
⊢ IsZero.{v_1, u_1}
    ((Y.H (coreE₂CohomologicalNat.deg (p, q) + 1)).obj
      (mk₁ (X₀ := coreE₂CohomologicalNat.i₀ (r + 1) (p, q) ⋯) (X₁ := coreE₂CohomologicalNat.i₀ r (p, q) ⋯)
        (homOfLE ⋯ : coreE₂CohomologicalNat.i₀ (r + 1) (p, q) ⋯ ⟶ coreE₂CohomologicalNat.i₀ r (p, q) ⋯)))
have hj : coreE₂CohomologicalNat.i₀ r (p, q) sorry ≤ WithBotTop.coe 0
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 (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
⊢ coreE₂CohomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe 0
have hj : (↑q : ℤ) - r + 2 ≤ 0
Tactic: simp only [coreE₂CohomologicalNat_i₀, 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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_2
⊢ (↑q : ℤ) - r + 2 ≤ 0
have hj : ∀ (this : 0 < (↑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.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
⊢ 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.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' : ℤ)
⊢ False
have hj : ∀ (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.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' : ℤ)
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) (p', q')
have left : (↑(p, q).1 : ℤ) + (r, 1 - r).1 = (↑(p', q').1 : ℤ)
Tactic: constructor