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

Goal state before:
pp: case h₁
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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁

Tactic:
dsimp

Goal state after:
case h₁
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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₀).map (homMk₁ (α.app 2 ≫ β.app 2) (α.app 3 ≫ β.app 3) ⋯) =
    (X.H n₀).map (homMk₁ (α.app 2) (α.app 3) ⋯) ≫ (X.H n₀).map (homMk₁ (β.app 2) (β.app 3) ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case h₂
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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₂

Tactic:
dsimp

Goal state after:
case h₂
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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (homMk₁ (α.app 1 ≫ β.app 1) (α.app 2 ≫ β.app 2) ⋯) =
    (X.H n₁).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case h₃
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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₃

Tactic:
dsimp

Goal state after:
case h₃
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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₂).map (homMk₁ (α.app 0 ≫ β.app 0) (α.app 1 ≫ β.app 1) ⋯) =
    (X.H n₂).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ (X.H n₂).map (homMk₁ (β.app 0) (β.app 1) ⋯)
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.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData

Tactic:
let hi := (X.kernelSequenceCycles_exact f₁ f₂ _ _ hn₂).fIsKernel

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 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₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData
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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f' = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁

Tactic:
let hi := (X.kernelSequenceCycles_exact f₁ f₂ _ _ hn₂).fIsKernel

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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
⊢ (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f' = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
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₂
⊢ Epi (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g

Tactic:
dsimp

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 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₂
⊢ Epi (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
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 : ℤ × ℤ
⊢ coreE₂Cohomological.i₀ 2 pq ⋯ = coreE₂Cohomological.i₁ pq

Tactic:
dsimp

Goal state after:
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
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 : ℤ × ℤ
⊢ coreE₂Cohomological.i₂ pq = coreE₂Cohomological.i₃ 2 pq ⋯

Tactic:
dsimp

Goal state after:
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)
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 : ℕ × ℕ
⊢ coreE₂CohomologicalNat.i₀ 2 pq ⋯ = coreE₂CohomologicalNat.i₁ pq

Tactic:
dsimp

Goal state after:
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
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 : ℕ × ℕ
⊢ coreE₂CohomologicalNat.i₂ pq = coreE₂CohomologicalNat.i₃ 2 pq ⋯

Tactic:
dsimp

Goal state after:
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)
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 : ℕ × ℕ
⊢ coreE₂HomologicalNat.i₀ 2 pq ⋯ = coreE₂HomologicalNat.i₁ pq

Tactic:
dsimp

Goal state after:
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)
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 : ℕ × ℕ
⊢ coreE₂HomologicalNat.i₂ pq = coreE₂HomologicalNat.i₃ 2 pq ⋯

Tactic:
dsimp

Goal state after:
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)
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₂
⊢ Mono (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp

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 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₂
⊢ Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
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₂
⊢ Epi (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g

Tactic:
dsimp

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 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₂
⊢ Epi (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
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₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
this : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0
⊢ z ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).g = 0

Tactic:
simpa only [zero_comp, Category.assoc, toCycles_i] using! this =≫ X.iCycles f₁ f₂ n₁

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₂
⊢ Mono (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp

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 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₂
⊢ Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)
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 + (r, 1 - r)).1 + (pq + (r, 1 - r)).2

Tactic:
dsimp

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₀ r : ℤ
pq : ℤ × ℤ
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_14
⊢ pq.1 + pq.2 + 1 = pq.1 + r + (pq.2 + (1 - r))
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' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43
⊢ WithBotTop.coe (hr.2 - r' + 2) = WithBotTop.coe (hr + (r, 1 - r)).2

Tactic:
dsimp

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₀ r r' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43
⊢ WithBotTop.coe (hr.2 - r' + 2) = WithBotTop.coe (hr.2 + (1 - r))
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' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_47
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_49
⊢ WithBotTop.coe ((hr + (r, 1 - r)).2 + r' - 1) = WithBotTop.coe (hr.2 + 1)

Tactic:
dsimp

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₀ r r' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_47
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_49
⊢ WithBotTop.coe (hr.2 + (1 - r) + r' - 1) = WithBotTop.coe (hr.2 + 1)
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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ : x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
⊢ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = 0

Tactic:
dsimp

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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ : x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
⊢ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
⊢ Mono sq.flip.f₂₄

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
⊢ Mono sq.f₃₄
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 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)

Tactic:
dsimp

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₂ = min (↑b₂ + (r - 1)).toNat l
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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ : x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
x₁ : A₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
⊢ π₁ ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp

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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
hx₂ : x₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
x₁ : A₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
⊢ π₁ ≫ x₂ = x₁ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.flip.f₁₃

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.f₁₂
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' : ℤ) (pq : ℤ × Fin l) (hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_24)
    (hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_26),
    ⟨(↑↑pq.2 - (r' - 2)).toNat, ⋯⟩ ≤ ⟨(↑↑pq.2 - (r - 2)).toNat, ⋯⟩

Tactic:
rintro r r' ⟨a, ⟨a', _⟩⟩ hr hrr'
    rw [Fin.mk_le_mk]
    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, ⟨a', isLt✝¹⟩).2 - (r' - 2)).toNat, ⋯⟩ = ↑(b, ⟨b', isLt✝⟩).2.castSucc

Tactic:
dsimp

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 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'
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_47
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_49
⊢ ↑(Fin.clamp (↑↑(b, ⟨b', isLt✝⟩).2 + (r' - 1)).toNat l) = ↑(a, ⟨a', isLt✝¹⟩).2.succ

Tactic:
dsimp

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 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_47
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_49
⊢ min (↑b' + (r' - 1)).toNat l = a' + 1
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₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g

Tactic:
dsimp

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₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)