awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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'
rw₁ rw₂ : data.i₀ r pq ⋯ = data.i₀ r pq ⋯
⊢ i₂ = data.i₂ pq'

Tactic:
rw [h₂, ← data.hc₀₂ r pq pq' hpq]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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' ⋯
rw₁ rw₂ : data.i₃ r pq' ⋯ = data.i₃ r pq' ⋯
⊢ i₃ = data.i₃ r pq' ⋯

Tactic:
rw [h₃, data.hc₁₃ r pq pq' hpq]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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
⊢ n₂ = data.deg pq'

Tactic:
simpa only [← hn₂, hn₁'] using data.hc r pq pq' hpq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ ((X.spectralSequence data).page r ⋯).d pq pq' =
    CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (Iso.hom (X.spectralSequencePageXIso data r hr pq i₂ i₃ i₄ i₅ h₂ h₃ h₄ h₅ n₀ n₁ n₂ hn₁' ⋯ ⋯) :
        ((X.spectralSequence data).page r ⋯).X pq ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫
          Iso.inv (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ h₀ h₁ ⋯ ⋯ n₁ n₂ n₃ ⋯ ⋯ ⋯) :
        X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯ ⟶ ((X.spectralSequence data).page r ⋯).X pq')

Tactic:
SpectralSequence.pageD_eq _ _ _ hr _ _ hpq ..

Premises used: CategoryTheory.Abelian.SpectralObject.E, dite, CategoryTheory.ShortComplex.homology, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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 : κ
i₀ i₁ i₂ i₃ : ι
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₂ : ℤ
h : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsZero.{v_1, u_1} (((X.spectralSequence data).page r ⋯).X pq) ↔
    IsZero.{v_1, u_1} (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)

Tactic:
Iso.isZero_iff (X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃
    h₀ h₁ h₂ h₃ n₀ n₁ n₂ h)

Premises used: CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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
⊢ i₁ ≤ i₂

Tactic:
simpa only [h₁, h₂] using data.le₁₂ pq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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 ⋯)))
rw : IsZero.{v_1, u_1} (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)
⊢ IsZero.{v_1, u_1} (((X.spectralSequence data).page r ⋯).X pq)

Tactic:
rw [X.isZero_spectralSequence_page_X_iff data r hr pq
    _ i₁ i₂ _ rfl h₁ h₂ rfl (n - 1) n (n + 1) hn]

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_iff, HSub.hSub, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)

Tactic:
isZero_E_of_isZero_H _ _ _ _ _ _ _ h

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)

Tactic:
exact isZero_E_of_isZero_H _ _ _ _ _ _ _ h

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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 : κ
h : IsZero.{v_1, u_1} ((X.H (data.deg pq)).obj (mk₁ (homOfLE ⋯)))
⊢ IsZero.{v_1, u_1} (((X.spectralSequence data).page r ⋯).X pq)

Tactic:
X.isZero_spectralSequence_page_X_of_isZero_H data r hr pq _ rfl _ _ rfl rfl h

Premises used: CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₂' : n₂ = data.deg pq'
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequencePageSc'Iso._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequencePageSc'Iso._auto_2
hn₃ : autoParam (n₂ + 1 = n₃) spectralSequencePageSc'Iso._auto_3
hn₄ : autoParam (n₃ + 1 = n₄) spectralSequencePageSc'Iso._auto_4
⊢ data.i₃ r pq'' ⋯ ≤ data.i₀ r pq ⋯

Tactic:
simpa only [← data.hc₁₃ r pq' pq'' hpq', data.hc₀₂ r pq pq' hpq]
          using data.le₁₂ pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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 (α :=
    ShortComplex.LeftHomologyData.K (S := ((X.spectralSequence data).page r hr).sc' pq pq' pq'')
        (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₁' hn₁ hn₂)) ⟶
      (((X.spectralSequence data).page r hr).sc' pq pq' pq'').X₂)
    (ShortComplex.LeftHomologyData.i
      (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₁' hn₁ hn₂)))
    (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ≫
      Iso.inv (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))

Tactic:
rfl

Premises used: CategoryTheory.Abelian.SpectralObject.E, CategoryTheory.ShortComplex.homology, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX, CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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'').X₂ ⟶
      ShortComplex.RightHomologyData.Q (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₁' hn₁ hn₂)))
    (ShortComplex.RightHomologyData.p
      (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₁' hn₁ hn₂)))
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (Iso.hom (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) :
        ((X.spectralSequence data).page r ⋯).X pq' ⟶ 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₂ ⋯ ⋯))

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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₂
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₁' ⋯ ⋯)))
    (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₁' ⋯ ⋯))))
    (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₁' ⋯ ⋯))))
⊢ 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₁' ⋯ ⋯)))

Tactic:
ext1
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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₁' ⋯ ⋯)))
    (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₁' ⋯ ⋯))))
    (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₁' ⋯ ⋯))))

Tactic:
simp [ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso]

Premises used: CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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₁ : autoParam (n₀ + 1 = n₁) spectralSequence_iso._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_iso._auto_2
⊢ r₀ ≤ r'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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₂
⊢ n₀ = n₁ - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ n₂ = n₁ + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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' : κ
hn₁ : data.deg pq' - 1 + 1 = data.deg pq'
hn₂ : data.deg pq' + 1 = data.deg pq' + 1
⊢ Eq (α := ((X.spectralSequence data).page r ⋯).homology pq' ⟶ ((X.spectralSequence data).page r' ⋯).X pq')
    (Iso.hom ((X.spectralSequence data).iso r r' pq' ⋯ ⋯) :
      ((X.spectralSequence data).page r ⋯).homology pq' ⟶ ((X.spectralSequence data).page r' ⋯).X pq')
    (Iso.hom
        (Iso.trans (Y := (((X.spectralSequence data).page r ⋯).sc' ((c r).prev pq') pq' ((c r).next pq')).homology)
          (((X.spectralSequence data).page r ⋯).homologyIsoSc' ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯)
          (Iso.trans (Y :=
            ShortComplex.LeftHomologyData.H (S :=
              ((X.spectralSequence data).page r hr).sc' ((c r).prev pq') pq' ((c r).next pq'))
              (ShortComplex.HomologyData.left
                (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯
                  (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯)
                  ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))
            (ShortComplex.LeftHomologyData.homologyIso
              (ShortComplex.HomologyData.left
                (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯
                  (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯)
                  ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))
            (Iso.symm
              (X.spectralSequencePageXIso data r' ⋯ pq' (data.i₀ r' pq' ⋯) (data.i₁ pq') (data.i₂ pq')
                (data.i₃ r' pq' ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))) :
      ((X.spectralSequence data).page r ⋯).homology pq' ⟶ ((X.spectralSequence data).page r' ⋯).X pq')

Tactic:
simp [spectralSequencePageXIso, spectralSequence, spectralSequenceHomologyData,
    SpectralSequence.homologyIso, SpectralSequence.homologyIso']

Premises used: CategoryTheory.Abelian.SpectralObject.spectralSequence, CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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
simp : q + 1 ≤ 0
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
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
⊢ q + 1 ≤ 0

Tactic:
lia