mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
n₀ n₁ n₂ : ℤ
⊢ 0 ≤ 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
n₀ n₁ n₂ : ℤ
⊢ 1 ≤ 3

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
n₀ n₁ n₂ : ℤ
⊢ 1 ≤ 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
n₀ n₁ n₂ : ℤ
⊢ 2 ≤ 3

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ 2 + ↑k
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨k + 1 + t, hq⟩) + 1
this : k < k + 1 + t
hpq : ∀ (a : ℤ) (b : Fin l), p + (2 + ↑k) = a → ¬↑(k + 1 + t) + (1 - (2 + ↑k)) = ↑↑b
⊢ t < l

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ 2 + ↑k
p : ℤ
t : ℕ
hq : k + 1 + t < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨k + 1 + t, hq⟩) + 1
this : k < k + 1 + t
hpq : ∀ (a : ℤ) (b : Fin l), p + (2 + ↑k) = a → ¬↑(k + 1 + t) + (1 - (2 + ↑k)) = ↑↑b
⊢ ↑k + 1 + ↑t + (1 - (2 + ↑k)) = ↑t

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ 2 + ↑k
p : ℤ
q : ℕ
hq : q < l
hn : n = p + ↑q + 1
hpq : ∀ (a : ℤ) (b : Fin l), p + (2 + ↑k) = a → ¬↑q + (1 - (2 + ↑k)) = ↑↑b
h : q ≤ k
⊢ ↑q - (2 + ↑k + 1 - 2) ≤ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁) ⊞ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₂ ≫ y₂ = y₁ ≫ biprod.desc ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)
⊢ y₁ = (y₁ ≫ biprod.fst) ≫ biprod.inl + (y₁ ≫ biprod.snd) ≫ biprod.inr

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
this : ↑q + r ≤ ↑l
t : ℕ
ht : ↑q + r + ↑t = ↑l
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬↑↑b + (1 - r) = ↑q
⊢ l - 1 - t < l

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
this : ↑q + r ≤ ↑l
t : ℕ
ht : ↑q + r + ↑t = ↑l
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬↑↑b + (1 - r) = ↑q
⊢ p - r + r = p

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
this : ↑q + r ≤ ↑l
t : ℕ
ht : ↑q + r + ↑t = ↑l
hpq : ∀ (a : ℤ) (b : Fin l), a + r = p → ¬↑↑b + (1 - r) = ↑q
⊢ ↑↑⟨l - 1 - t, ⋯⟩ + (1 - r) = ↑q

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
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₂
⊢ n₀ = n₁ - 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject 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⟩) - 1
h : ↑l < ↑q + r
⊢ l ≤ (↑q + (r - 1)).toNat

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject 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⟩) - 1
h : ↑l < ↑q + r
⊢ l ≤ (↑q + r).toNat

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
⊢ 0 ≤ ↑p + r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
⊢ 0 ≤ ↑q + 1 - r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case left
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p, q).1 + (r, 1 - r).1 = ↑(p', q').1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case right
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p, q).2 + (r, 1 - r).2 = ↑(p', q').2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₀ n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₁ : n₀ + 1 = data.deg pq
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
⊢ n₀ = data.deg pq - 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₂ n₃ : ℤ
hn₃ : n₂ + 1 = n₃
hn₂ : data.deg pq + 1 = n₂
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
⊢ n₂ = data.deg pq + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
⊢ 0 ≤ ↑p - r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
n₃ : ℤ
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
hn₃ : data.deg pq + 1 + 1 = n₃
hn₂ : data.deg pq + 1 = data.deg pq + 1
⊢ n₃ = data.deg pq + 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
⊢ 0 ≤ ↑q - 1 + r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case left
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').1 + (r, 1 - r).1 = ↑(p, q).1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case right
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').2 + (r, 1 - r).2 = ↑(p, q).2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
⊢ data.deg pq + 1 + 1 = data.deg pq + 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
⊢ 0 ≤ ↑p - r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
⊢ 0 ≤ ↑q + r - 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₀ - 1 + 1 = n₀

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case left
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).1 + (-r, r - 1).1 = ↑(p', q').1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case right
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).2 + (-r, r - 1).2 = ↑(p', q').2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv ≫ X.iCycles (𝟙 i₀) f n₀ = X.toCycles (𝟙 i₀) f f ⋯ n₀ ≫ X.iCycles (𝟙 i₀) f n₀

Tactic:
toCycles_i

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv ≫ X.iCycles (𝟙 i₀) f n₀ = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₁ + 1 = n₁ + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
this : data.deg pq + 1 = data.deg pq'
⊢ n₁ = data.deg pq

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
⊢ 0 ≤ ↑p + r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
p' : ℕ
hp' : ↑p + r = ↑p'
⊢ 0 ≤ ↑q + 1 - r

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
this : data.deg pq' + 1 = data.deg pq''
⊢ n₃ = data.deg pq''

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ h.i = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.iCycles (𝟙 i) f n₁

Tactic:
toCycles_i

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ h.i = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case left
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p', q').1 + (-r, r - 1).1 = ↑(p, q).1

Tactic:
lia

Goal state after: