awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X := (X.H n₀).obj (mk₁ f₅)) (Y := (X.H n₀).obj (mk₁ f₅))
    ((X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 3)) ⋯))
have h₁ : homMk₁ (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 3)) sorry = 𝟙 (mk₁ f₅)
Tactic: convert! (inferInstance : Epi ((X.H n₀).map (𝟙 _)))
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂)
have h₂ : IsIso (X := (X.H n₁).obj (mk₁ f₄)) (Y := (X.H n₁).obj (mk₁ f₄))
  ((X.H n₁).map (homMk₁ (𝟙 i₃) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X := (X.H n₁).obj (mk₁ f₄)) (Y := (X.H n₁).obj (mk₁ f₄))
    ((X.H n₁).map (homMk₁ (𝟙 i₃) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) ⋯))
have h₁ : homMk₁ (𝟙 i₃) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) sorry = 𝟙 (mk₁ f₄)
Tactic: convert! (inferInstance : IsIso ((X.H n₁).map (𝟙 _)))
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
Goal:
C : Type u_1
ι' : 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_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ =
    X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂
have rw : Eq (α :=
  X'.E (homOfLE sorry) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶
    X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE sorry) n₀ n₁ n₂ hn₁ hn₂)
  (X'.map (homOfLE sorry) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE sorry)
    (fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ ≫ fourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅) n₀ n₁ n₂ sorry sorry)
  (X'.map (homOfLE sorry) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE sorry)
    (fourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ sorry hi₂₃ hi₃₄ hi₄₅ ≫ fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ sorry) n₀ n₁ n₂ sorry sorry)
Tactic: rw [← map_comp .., ← map_comp ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
⊢ i₁ = data.i₀ r₀ pq ⋯
have rw : data.i₁ pq = data.i₀ r₀ pq sorry
Tactic: rw [hi₁, ← data.hi₀₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
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 [hi₁, ← data.hi₀₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
⊢ i₂ = data.i₃ r₀ pq ⋯
have rw : data.i₂ pq = data.i₃ r₀ pq sorry
Tactic: rw [hi₂, data.hi₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
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 [hi₂, data.hi₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
⊢ i₁ = data.i₀ r₀ pq ⋯
have rw : data.i₁ pq = data.i₀ r₀ pq sorry
Tactic: rw [hi₁, ← data.hi₀₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
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 [hi₁, ← data.hi₀₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
⊢ i₂ = data.i₃ r₀ pq ⋯
have rw : data.i₂ pq = data.i₃ r₀ pq sorry
Tactic: rw [hi₂, data.hi₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
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 [hi₂, data.hi₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
      (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom)
have obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁),
  Eq (α := ((X.spectralSequence data).page r₀ sorry).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE sorry)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ sorry pq i₁ i₁ i₂ i₂ sorry hi₁ hi₂ sorry (n₁ - 1) n₁ n₂ hn₁' sorry sorry) ≫
      (X.EIsoH (homOfLE sorry) (n₁ - 1) n₁ n₂ hn₁ hn₂).hom)
Tactic: obtain rfl : n₀ = n₁ - 1 := by lia
Cleared hypotheses: n₀, hn₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯) ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).hom)
have obtain : Eq (α := ((X.spectralSequence data).page r₀ sorry).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE sorry)))
  (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
  (Iso.hom (X.spectralSequencePageXIso data r₀ sorry pq i₁ i₁ i₂ i₂ sorry hi₁ hi₂ sorry (n₁ - 1) n₁ (n₁ + 1) hn₁' sorry sorry) ≫
    (X.EIsoH (homOfLE sorry) (n₁ - 1) n₁ (n₁ + 1) hn₁ sorry).hom)
Tactic: obtain rfl := hn₂
Cleared hypotheses: n₂, hn₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
⊢ i₁ = data.i₀ r₀ pq ⋯
have rw : data.i₁ pq = data.i₀ r₀ pq sorry
Tactic: rw [hi₁, ← data.hi₀₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
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 [hi₁, ← data.hi₀₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
⊢ i₂ = data.i₃ r₀ pq ⋯
have rw : data.i₂ pq = data.i₃ r₀ pq sorry
Tactic: rw [hi₂, data.hi₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
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 [hi₂, data.hi₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯))
have obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁),
  Eq (α := (X.H n₁).obj (mk₁ (homOfLE sorry)) ⟶ ((X.spectralSequence data).page r₀ sorry).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE sorry) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ sorry pq i₁ i₁ i₂ i₂ sorry hi₁ hi₂ sorry (n₁ - 1) n₁ n₂ hn₁' sorry sorry))
Tactic: obtain rfl : n₀ = n₁ - 1 := by lia
Cleared hypotheses: n₀, hn₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯))
have obtain : Eq (α := (X.H n₁).obj (mk₁ (homOfLE sorry)) ⟶ ((X.spectralSequence data).page r₀ sorry).X pq)
  (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
  ((X.EIsoH (homOfLE sorry) (n₁ - 1) n₁ (n₁ + 1) hn₁ sorry).inv ≫
    Iso.inv (X.spectralSequencePageXIso data r₀ sorry pq i₁ i₁ i₂ i₂ sorry hi₁ hi₂ sorry (n₁ - 1) n₁ (n₁ + 1) hn₁' sorry sorry))
Tactic: obtain rfl := hn₂
Cleared hypotheses: n₂, hn₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ j = data.i₂ pq'
have rw : data.i₁ pq = data.i₂ pq'
Tactic: rw [hj, ← data.hc₀₂ r₀ pq pq' hpq, data.hi₀₁ pq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
rw : data.i₁ pq = data.i₂ pq'
⊢ j = data.i₂ pq'
have rw₁ : data.i₁ pq = data.i₀ r₀ pq sorry
Tactic: rw [hj, ← data.hc₀₂ r₀ pq pq' hpq, data.hi₀₁ pq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
rw : data.i₁ pq = data.i₂ pq'
rw₁ : data.i₁ pq = data.i₀ r₀ pq ⋯
⊢ j = data.i₂ pq'
have rw₂ : data.i₁ pq = data.i₁ pq
Tactic: rw [hj, ← data.hc₀₂ r₀ pq pq' hpq, data.hi₀₁ pq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ n' = data.deg pq'
have rw : n + 1 = data.deg pq'
Tactic: rw [← hn', hn, data.hc r₀ pq pq' hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
rw : n + 1 = data.deg pq'
⊢ n' = data.deg pq'
have rw₁ : data.deg pq + 1 = data.deg pq'
Tactic: rw [← hn', hn, data.hc r₀ pq pq' hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.FirstPage (goal)
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
rw : n + 1 = data.deg pq'
rw₁ : data.deg pq + 1 = data.deg pq'
⊢ n' = data.deg pq'
have rw₂ : data.deg pq' = data.deg pq'
Tactic: rw [← hn', hn, data.hc r₀ pq pq' hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (goal)
Goal:
ι : Type u_2
κ : Type u_3
inst : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
⊢ i₀' ≤ i₀
have rw : data.i₀ r' pq' sorry ≤ data.i₀ r pq' sorry
Tactic: rw [hi₀', hi₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (hypothesis)
Goal:
ι : Type u_2
κ : Type u_3
inst : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₀ i₁ : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
⊢ i₀ ≤ i₁
have this : data.i₀ r pq' sorry ≤ data.i₁ pq'
Tactic: have := data.le₀₁ r pq'
-- 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₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
⊢ WithBotTop.coe (pq.2 - r + 2) ≤ WithBotTop.coe pq.2
have simp : pq.2 - r + 2 ≤ pq.2
Tactic: simp
-- 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₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
⊢ WithBotTop.coe (pq.2 + 1) ≤ WithBotTop.coe (pq.2 + r - 1)
have simp : pq.2 + 1 ≤ pq.2 + r - 1
Tactic: simp
-- 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₀ r : ℤ
pq : ℤ × ℤ
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_7
⊢ pq.1 + pq.2 + 1 = (pq + (r, 1 - r)).1 + (pq + (r, 1 - r)).2
have dsimp : pq.1 + pq.2 + 1 = pq.1 + r + (pq.2 + (1 - r))
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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r + 2) ≤ WithBotTop.coe (↑pq.2 : ℤ)
have simp : (↑pq.2 : ℤ) - r + 2 ≤ (↑pq.2 : ℤ)
Tactic: simp