mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
q'' : ℤ
hq'' : q'' + 1 = q
g : X ⟶ K.X q''
hf : (g ≫ K.d q'' q) ≫ K.d q q' = 0
⊢ p + (n - 1) = q''

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ p' + (n + 1) = q

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : (n + 1).negOnePow • δ n (n + 1) (Cochain.toSingleMk f h) = 0
⊢ p' + (n + 1) = q

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ p' + (n + 1) = q

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
hα : δ (n - 1) n α = ↑(toSingleMk f h p' hp' hf)
⊢ p'' + (n - 1) = q

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ p'' + (n - 1) = q

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ ∃ β, δ (n - 1) n β = ↑(toSingleMk (K.d p p'' ≫ g) h p' hp' hf)

Tactic:
exact ⟨n.negOnePow • Cochain.toSingleMk g (by lia),
      by simp [Cochain.δ_toSingleMk _ _ _ _ h, smul_smul]⟩

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
inst✝² : X₁.HasTensor Y₁
inst✝¹ : X₂.HasTensor Y₂
inst✝ : X₃.HasTensor Y₃
⊢ tensorHom f₁ g₁ ≫ tensorHom f₂ g₂ = tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂)

Tactic:
ext
  simp

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

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 j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₀ = n₁ - 1

Tactic:
lia

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

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 j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hx : X.δ f g n₀ n₁ hn₁ ≫ x = 0
⊢ n₀ = n₁ - 1

Tactic:
lia

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

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 j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ n - 1 + 1 = n

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
x✝ : ↑((fun i ↦ i.1 + i.2) ⁻¹' {n})
i₁ i₂ : ℕ
hi : i₁ + i₂ = n
⊢ i₁ < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
x✝ : ↑((fun i ↦ i.1 + i.2) ⁻¹' {n})
i₁ i₂ : ℕ
hi : i₁ + i₂ = n
⊢ i₂ < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
x✝ : ↑{i | i.1 + i.2.1 + i.2.2 = n}
i₁ i₂ i₃ : ℕ
hi : i₁ + i₂ + i₃ = n
⊢ i₁ < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
x✝ : ↑{i | i.1 + i.2.1 + i.2.2 = n}
i₁ i₂ i₃ : ℕ
hi : i₁ + i₂ + i₃ = n
⊢ i₂ < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
x✝ : ↑{i | i.1 + i.2.1 + i.2.2 = n}
i₁ i₂ i₃ : ℕ
hi : i₁ + i₂ + i₃ = n
⊢ i₃ < n + 1

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)

Tactic:
by rw [X.cyclesMap_id]; infer_instance

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

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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₀ - 1 + 1 = n₀

Tactic:
lia

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

Goal state before:
pp: case fst
u : ℤ × ℤ
i✝ j✝ j'✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i✝.fst + u.fst = ↑j'✝.fst ∧ ↑i✝.snd + u.snd = ↑j'✝.snd
⊢ j✝.fst = j'✝.fst

Tactic:
lia

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

Goal state before:
pp: case snd
u : ℤ × ℤ
i✝ j✝ j'✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i✝.fst + u.fst = ↑j'✝.fst ∧ ↑i✝.snd + u.snd = ↑j'✝.snd
⊢ j✝.snd = j'✝.snd

Tactic:
lia

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

Goal state before:
pp: case fst
u : ℤ × ℤ
i✝ i'✝ j✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i'✝.fst + u.fst = ↑j✝.fst ∧ ↑i'✝.snd + u.snd = ↑j✝.snd
⊢ i✝.fst = i'✝.fst

Tactic:
lia

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

Goal state before:
pp: case snd
u : ℤ × ℤ
i✝ i'✝ j✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i'✝.fst + u.fst = ↑j✝.fst ∧ ↑i'✝.snd + u.snd = ↑j✝.snd
⊢ i✝.snd = i'✝.snd

Tactic:
lia

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

Goal state before:
pp: case fst
l : ℕ
u : ℤ × ℤ
i✝ j✝ j'✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i✝.fst + u.fst = j'✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j'✝.snd
⊢ j✝.fst = j'✝.fst

Tactic:
lia

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

Goal state before:
pp: case snd
l : ℕ
u : ℤ × ℤ
i✝ j✝ j'✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i✝.fst + u.fst = j'✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j'✝.snd
⊢ ↑j✝.snd = ↑j'✝.snd

Tactic:
lia

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

Goal state before:
pp: case fst
l : ℕ
u : ℤ × ℤ
i✝ i'✝ j✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i'✝.fst + u.fst = j✝.fst ∧ ↑↑i'✝.snd + u.snd = ↑↑j✝.snd
⊢ i✝.fst = i'✝.fst

Tactic:
lia

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

Goal state before:
pp: case snd
l : ℕ
u : ℤ × ℤ
i✝ i'✝ j✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i'✝.fst + u.fst = j✝.fst ∧ ↑↑i'✝.snd + u.snd = ↑↑j✝.snd
⊢ ↑i✝.snd = ↑i'✝.snd

Tactic:
lia

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

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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₀ = n₁ - 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 j k : ι
f : i ⟶ j
g : j ⟶ k
hf : IsIso f
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
by
  simpa only [Preadditive.IsIso.comp_left_eq_zero] using X.zero₃ f g _ rfl n₀ n₁

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{?u.6, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℤ × ℤ
⊢ WithBotTop.coe (pq.2 - 2 + 2) = WithBotTop.coe pq.2

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{?u.6, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℤ × ℤ
⊢ WithBotTop.coe (pq.2 + 1) = WithBotTop.coe (pq.2 + 2 - 1)

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{?u.6, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (↑pq.2 - 2 + 2) = WithBotTop.coe ↑pq.2

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{?u.6, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (↑pq.2 + 1) = WithBotTop.coe (↑pq.2 + 2 - 1)

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{?u.6, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (-↑pq.2 - 2 + 2) = WithBotTop.coe (-↑pq.2)

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{?u.6, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (-↑pq.2 + 1) = WithBotTop.coe (-↑pq.2 + 2 - 1)

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : 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₂
⊢ n₀ = n₁ - 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) =
    0

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₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
⊢ pq.2 - r + 2 ≤ 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₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
⊢ pq.2 + 1 ≤ pq.2 + r - 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₀ r : ℤ
pq : ℤ × ℤ
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_14
⊢ pq.1 + pq.2 + 1 = pq.1 + r + (pq.2 + (1 - 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₀ r : ℤ
pq : ℤ × ℤ
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_16
⊢ WithBotTop.coe (pq.2 - r + 2) = WithBotTop.coe (pq.2 + (1 - r) + 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₀ r : ℤ
pq : ℤ × ℤ
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_20
⊢ WithBotTop.coe pq.2 = WithBotTop.coe (pq.2 + (1 - r) + r - 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₀ r r' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ 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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ ↑pq.2 - r + 2 ≤ ↑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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ ↑pq.2 + 1 ≤ ↑pq.2 + r - 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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ ↑pq.1 + ↑pq.2 + 1 = ↑pq'.1 + ↑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₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ 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₀ : ℤ
l : ℕ
r p : ℤ
q : ℕ
hq : q < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_5
⊢ ↑q - (r - 2) ≤ ↑q

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₀ : ℤ
l : ℕ
x✝³ : ℤ
x✝² x✝¹ : ℤ × Fin l
x✝ : (ComplexShape.spectralSequenceFin l (x✝³, 1 - x✝³)).Rel x✝² x✝¹
h₁ : x✝².1 + (x✝³, 1 - x✝³).1 = x✝¹.1
h₂ : ↑↑x✝².2 + (x✝³, 1 - x✝³).2 = ↑↑x✝¹.2
⊢ autoParam (2 ≤ x✝³) SpectralSequenceDataCore._auto_14 → x✝².1 + ↑↑x✝².2 + 1 = x✝¹.1 + ↑↑x✝¹.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₀ : ℤ
l : ℕ
r : ℤ
⊢ ∀ (pq pq' : ℤ × Fin l),
    (ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq' →
      ∀ (hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_16), ⟨(↑↑pq.2 - (r - 2)).toNat, ⋯⟩ = pq'.2.succ

Tactic:
rintro ⟨a₁, ⟨a₂, _⟩⟩ ⟨b₁, ⟨b₂, _⟩⟩ ⟨h₁, h₂⟩ hr

Goal state after:
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₀ : ℤ
l : ℕ
r a₁ : ℤ
a₂ : ℕ
isLt✝¹ : a₂ < l
b₁ : ℤ
b₂ : ℕ
isLt✝ : b₂ < l
h₁ : (a₁, ⟨a₂, isLt✝¹⟩).1 + (r, 1 - r).1 = (b₁, ⟨b₂, isLt✝⟩).1
h₂ : ↑↑(a₁, ⟨a₂, isLt✝¹⟩).2 + (r, 1 - r).2 = ↑↑(b₁, ⟨b₂, isLt✝⟩).2
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_16
⊢ ⟨(↑↑(a₁, ⟨a₂, isLt✝¹⟩).2 - (r - 2)).toNat, ⋯⟩ = (b₁, ⟨b₂, isLt✝⟩).2.succ
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₀ : ℤ
l : ℕ
r : ℤ
⊢ ∀ (pq pq' : ℤ × Fin l),
    (ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq' →
      autoParam (2 ≤ r) SpectralSequenceDataCore._auto_20 → pq.2.castSucc = Fin.clamp (↑↑pq'.2 + (r - 1)).toNat l

Tactic:
rintro ⟨a₁, ⟨a₂, _⟩⟩ ⟨b₁, ⟨b₂, _⟩⟩ ⟨h₁, h₂⟩ hr

Goal state after:
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₀ : ℤ
l : ℕ
r a₁ : ℤ
a₂ : ℕ
isLt✝¹ : a₂ < l
b₁ : ℤ
b₂ : ℕ
isLt✝ : b₂ < l
h₁ : (a₁, ⟨a₂, isLt✝¹⟩).1 + (r, 1 - r).1 = (b₁, ⟨b₂, isLt✝⟩).1
h₂ : ↑↑(a₁, ⟨a₂, isLt✝¹⟩).2 + (r, 1 - r).2 = ↑↑(b₁, ⟨b₂, isLt✝⟩).2
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_20
⊢ (a₁, ⟨a₂, isLt✝¹⟩).2.castSucc = Fin.clamp (↑↑(b₁, ⟨b₂, isLt✝⟩).2 + (r - 1)).toNat l
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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_24
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_26
⊢ (↑↑(a, ⟨a', isLt✝⟩).2 - (r' - 2)).toNat ≤ (↑↑(a, ⟨a', isLt✝⟩).2 - (r - 2)).toNat

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₂'
⊢ 0 ≤ 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_34
⊢ (↑↑(a, ⟨a', isLt✝⟩).2 + (r - 1)).toNat ≤ (↑↑(a, ⟨a', isLt✝⟩).2 + (r' - 1)).toNat

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₂'
⊢ 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₂'
⊢ 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₂'
⊢ 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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝¹ : a' < l
b : ℤ
b' : ℕ
isLt✝ : b' < l
h₁ : (a, ⟨a', isLt✝¹⟩).1 + (r, 1 - r).1 = (b, ⟨b', isLt✝⟩).1
h₂ : ↑↑(a, ⟨a', isLt✝¹⟩).2 + (r, 1 - r).2 = ↑↑(b, ⟨b', isLt✝⟩).2
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43
⊢ (↑a' - (r' - 2)).toNat = b'

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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ -↑pq.2 - r + 2 ≤ -↑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₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ -↑pq.2 + 1 ≤ -↑pq.2 + r - 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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ -↑pq.1 - ↑pq.2 + 1 = -↑pq'.1 - ↑pq'.2

Tactic:
lia

Goal state after: