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 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₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ≫ X.pOpcycles f₂ f₃ n₁ = 0

Tactic:
simp

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₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ = 0

Tactic:
simp

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₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ (parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).map
        WalkingParallelPairHom.right ≫
      (Iso.refl
          ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
            WalkingParallelPair.one)).hom =
    (Iso.refl
          ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
            WalkingParallelPair.zero)).hom ≫
      (parallelPair (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) 0).map WalkingParallelPairHom.right

Tactic:
simp

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.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g =
    { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology,
          X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles,
          X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃,
          f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι,
          g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles, zero := ⋯ }.g ≫
      (Iso.refl
          { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology,
              X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles,
              X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃,
              f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι,
              g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles, zero := ⋯ }.X₃).hom

Tactic:
simp

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₁₂
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₁ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
x₁ : A₂ ⟶ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).X₁
hx₁ : π₂ ≫ z = x₁ ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp at x₁ hx₁

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₁₂
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₁ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
x₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁)
hx₁ : π₂ ≫ z = x₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
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
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₂ ⋯)) ≫
      biprod.fst =
    0 ≫ biprod.fst

Tactic:
simp

Goal state after:
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
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₂ ⋯)) ≫
      biprod.snd =
    0 ≫ biprod.snd

Tactic:
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
⊢ WithBotTop.coe (pq.2 - r + 2) ≤ WithBotTop.coe pq.2

Tactic:
simp

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 : 2 ≤ r
⊢ pq.2 - r + 2 ≤ pq.2
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₀ : ℤ
pq : ℤ × ℤ
⊢ WithBotTop.coe pq.2 ≤ WithBotTop.coe (pq.2 + 1)

Tactic:
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
⊢ WithBotTop.coe (pq.2 + 1) ≤ WithBotTop.coe (pq.2 + r - 1)

Tactic:
simp

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 : 2 ≤ r
⊢ pq.2 + 1 ≤ pq.2 + r - 1
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 + (r, 1 - r)).2 + 1)

Tactic:
simp

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_16
⊢ WithBotTop.coe (pq.2 - r + 2) = WithBotTop.coe (pq.2 + (1 - r) + 1)
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 + (r, 1 - r)).2 + r - 1)

Tactic:
simp

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_20
⊢ WithBotTop.coe pq.2 = WithBotTop.coe (pq.2 + (1 - r) + r - 1)
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'
⊢ WithBotTop.coe (pq.2 - r' + 2) ≤ WithBotTop.coe (pq.2 - r + 2)

Tactic:
simp

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' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ 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' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ WithBotTop.coe (pq.2 + r - 1) ≤ WithBotTop.coe (pq.2 + r' - 1)

Tactic:
simp

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' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ 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 : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ WithBotTop.coe (↑pq.2 - r + 2) ≤ WithBotTop.coe ↑pq.2

Tactic:
simp

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 : 2 ≤ r
⊢ ↑pq.2 - r + 2 ≤ ↑pq.2
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₀ : ℤ
pq : ℕ × ℕ
⊢ WithBotTop.coe ↑pq.2 ≤ WithBotTop.coe (↑pq.2 + 1)

Tactic:
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
⊢ WithBotTop.coe (↑pq.2 + 1) ≤ WithBotTop.coe (↑pq.2 + r - 1)

Tactic:
simp

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 : 2 ≤ r
⊢ ↑pq.2 + 1 ≤ ↑pq.2 + r - 1
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'
⊢ WithBotTop.coe (↑pq.2 - r' + 2) ≤ WithBotTop.coe (↑pq.2 - r + 2)

Tactic:
simp

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' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ 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' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ WithBotTop.coe (↑pq.2 + r - 1) ≤ WithBotTop.coe (↑pq.2 + r' - 1)

Tactic:
simp

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' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ r'
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square C)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).op.f₁₂ ≫ φ.unop.τ₂.op).unop = (φ.unop.τ₄.op ≫ (Opposite.unop Y✝).op.f₁₂).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square C)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).op.f₁₃ ≫ φ.unop.τ₃.op).unop = (φ.unop.τ₄.op ≫ (Opposite.unop Y✝).op.f₁₃).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square C)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).op.f₂₄ ≫ φ.unop.τ₁.op).unop = (φ.unop.τ₂.op ≫ (Opposite.unop Y✝).op.f₂₄).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square C)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).op.f₃₄ ≫ φ.unop.τ₁.op).unop = (φ.unop.τ₃.op ≫ (Opposite.unop Y✝).op.f₃₄).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square Cᵒᵖ)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).unop.f₁₂ ≫ φ.unop.τ₂.unop).op = (φ.unop.τ₄.unop ≫ (Opposite.unop Y✝).unop.f₁₂).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square Cᵒᵖ)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).unop.f₁₃ ≫ φ.unop.τ₃.unop).op = (φ.unop.τ₄.unop ≫ (Opposite.unop Y✝).unop.f₁₃).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square Cᵒᵖ)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).unop.f₂₄ ≫ φ.unop.τ₁.unop).op = (φ.unop.τ₂.unop ≫ (Opposite.unop Y✝).unop.f₂₄).op

Tactic:
simp

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₂₃ : 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₂ ≫ X.δ f₁ f₂₃ n₁ n₂ ⋯ = 0

Tactic:
simpa using hx₂ =≫ biprod.snd

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
⊢ ⟨(↑↑(p, ⟨q, hq⟩).2 - (r - 2)).toNat, ⋯⟩ ≤ (p, ⟨q, hq⟩).2.castSucc

Tactic:
simp

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 p : ℤ
q : ℕ
hq : q < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_5
⊢ ↑q - (r - 2) ≤ ↑q
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : (Square Cᵒᵖ)ᵒᵖ
φ : X✝ ⟶ Y✝
⊢ ((Opposite.unop X✝).unop.f₃₄ ≫ φ.unop.τ₁.unop).op = (φ.unop.τ₃.unop ≫ (Opposite.unop Y✝).unop.f₃₄).op

Tactic:
simp

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₂₃ : 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.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁
hx₁ : π₁ ≫ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ = x₁ ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp at x₁ hx₁

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₂
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Tactic:
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
⊢ WithBotTop.coe (-↑pq.2 - r + 2) ≤ WithBotTop.coe (-↑pq.2)

Tactic:
simp

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 : 2 ≤ r
⊢ -↑pq.2 - r + 2 ≤ -↑pq.2
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₀ : ℤ
pq : ℕ × ℕ
⊢ WithBotTop.coe (-↑pq.2) ≤ WithBotTop.coe (-↑pq.2 + 1)

Tactic:
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
⊢ WithBotTop.coe (-↑pq.2 + 1) ≤ WithBotTop.coe (-↑pq.2 + r - 1)

Tactic:
simp

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 : 2 ≤ r
⊢ -↑pq.2 + 1 ≤ -↑pq.2 + r - 1
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'
⊢ WithBotTop.coe (-↑pq.2 - r' + 2) ≤ WithBotTop.coe (-↑pq.2 - r + 2)

Tactic:
simp

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' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ 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' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ WithBotTop.coe (-↑pq.2 + r - 1) ≤ WithBotTop.coe (-↑pq.2 + r' - 1)

Tactic:
simp

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' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ r'
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₂
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ = 0

Tactic:
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
E : SpectralObject C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = coreE₂Cohomological.deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (ComplexShape.up' (r, 1 - r)).Rel (pq - (r, 1 - r)) pq

Tactic:
simp

Goal state after: