mathlib-initiative/mathlib-tactics huggingface dataset:
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₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ i ≤ j

Tactic:
simpa using

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₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ data.i₁ pq' ≤ data.i₂ pq'
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₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ j ≤ k

Tactic:
simpa using

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₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ data.i₁ pq ≤ data.i₂ pq
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 pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : n + 1 = n'
⊢ ((X.spectralSequence data).page r₀ ⋯).d pq pq' =
    (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom ≫
      X.δ (homOfLE ⋯) (homOfLE ⋯) n n' hn' ≫ (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv

Tactic:
simpa using

Goal state after:
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 pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : n + 1 = n'
⊢ ((X.spectralSequence data).page r₀ ⋯).d pq pq' =
    (X.spectralSequencePageXIso data r₀ ⋯ pq j j k k ⋯ hj hk ⋯ (n - 1) n n' hn ⋯ ⋯).hom ≫
      X.d (𝟙 i) (homOfLE ⋯) (𝟙 j) (homOfLE ⋯) (𝟙 k) (n - 1) n n' (n' + 1) ⋯ ⋯ ⋯ ≫
        (X.spectralSequencePageXIso data r₀ ⋯ pq' i i j j ⋯ hi ⋯ ⋯ n n' (n' + 1) ⋯ ⋯ ⋯).inv
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₀ i₁ : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
this : data.i₀ r pq' ⋯ ≤ data.i₁ pq'
⊢ i₀ ≤ i₁

Tactic:
simpa using

Goal state after:
ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₀ i₁ : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
this : data.i₀ r pq' ⋯ ≤ data.i₁ pq'
⊢ data.i₀ r pq' ⋯ ≤ data.i₁ pq'
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₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂ = x

Tactic:
by
  dsimp only [descE]
  rw [← Category.assoc]
  apply (X.cokernelSequenceE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂).g_desc

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq' : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
⊢ i₁ ≤ i₂

Tactic:
simpa using

Goal state after:
ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq' : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
⊢ data.i₁ pq' ≤ data.i₂ pq'
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₂ i₃ : ι
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
⊢ i₂ ≤ i₃

Tactic:
simpa using

Goal state after:
ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₂ i₃ : ι
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
⊢ data.i₂ pq' ≤ data.i₃ r pq' ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
⊢ i₃ ≤ i₃'

Tactic:
simpa using

Goal state after:
ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
⊢ data.i₃ r pq' ⋯ ≤ data.i₃ r' pq' ⋯
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.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0

Tactic:
simpa using

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₂ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
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

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
sq : Square C
F : C ⥤ D
⊢ F.map sq.f₁₂ ≫ F.map sq.f₂₄ = F.map sq.f₁₃ ≫ F.map sq.f₃₄

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
sq : Square C
F : C ⥤ D
⊢ F.map sq.f₁₂ ≫ F.map sq.f₂₄ = F.map sq.f₁₃ ≫ F.map 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₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq ⋯
hi₀ : i₀ = data.i₀ r pq ⋯
⊢ i₀' ≤ i₀

Tactic:
simpa using

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₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq'
n : ℤ
hn : n = data.deg pq + 1
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq ⋯
hi₀ : i₀ = data.i₀ r pq ⋯
⊢ data.i₀ r' pq ⋯ ≤ data.i₀ r pq ⋯
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₂
⊢ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ ≫ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ =
    X.opcyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₁

Tactic:
simpa using

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₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₂ f₃ n₁ =
    X.pOpcycles f₁₂ f₃ n₁ ≫ X.opcyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ 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₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq ⋯
hi₃' : i₃' = data.i₃ r' pq ⋯
⊢ i₃ ≤ i₃'

Tactic:
simpa using

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₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq ⋯
hi₃' : i₃' = data.i₃ r' pq ⋯
⊢ data.i₃ r pq ⋯ ≤ data.i₃ r' pq ⋯
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₂
⊢ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂ =
    X.cyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁

Tactic:
simpa using

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₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.iCycles f₁ f₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.cyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.iCycles f₁ f₂₃ n₁
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'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_3
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_5
⊢ i₃ = data.i₃ r pq' ⋯

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

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'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_3
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_5
⊢ n₂ = data.deg pq'

Tactic:
simpa using

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_3
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_5
⊢ data.deg pq + 1 = data.deg pq'
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₁).hom ≫ X.toCycles (𝟙 i₀) f f ⋯ n₀ = 𝟙 (X.cycles (𝟙 i₀) f n₀)

Tactic:
simpa using

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₁).hom ≫ X.toCycles (𝟙 i₀) f f ⋯ n₀ = 𝟙 (X.cycles (𝟙 i₀) f 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₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.toCycles (𝟙 i₀) f f ⋯ n₀ ≫ (X.cyclesIsoH f n₀ n₁ hn₁).hom = 𝟙 ((X.H n₀).obj (mk₁ f))

Tactic:
simpa using

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.toCycles (𝟙 i₀) f f ⋯ n₀ ≫ (X.cyclesIsoH f n₀ n₁ hn₁).hom = 𝟙 ((X.H n₀).obj (mk₁ f))
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'
⊢ data.i₃ r pq'' ⋯ ≤ data.i₀ r pq ⋯

Tactic:
simpa using

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 ι
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'
⊢ data.i₁ pq' ≤ data.i₂ pq'
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.fromOpcycles f (𝟙 i₁) f ⋯ n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = 𝟙 (X.opcycles f (𝟙 i₁) n₁)

Tactic:
simpa using

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.fromOpcycles f (𝟙 i₁) f ⋯ n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = 𝟙 (X.opcycles f (𝟙 i₁) 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₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.opcyclesIsoH f n₀ n₁ hn₁).inv ≫ X.fromOpcycles f (𝟙 i₁) f ⋯ n₁ = 𝟙 ((X.H n₁).obj (mk₁ f))

Tactic:
simpa using

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.opcyclesIsoH f n₀ n₁ hn₁).inv ≫ X.fromOpcycles f (𝟙 i₁) f ⋯ n₁ = 𝟙 ((X.H n₁).obj (mk₁ f))
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case refine_2
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'
⊢ (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂' ⋯
          ⋯).hom ≫
      (X.dShortComplex (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ n₃
          n₄ hn₁ hn₂ hn₃ hn₄).g =
    ((page X data r hr).sc' pq pq' pq'').g ≫
      (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃ n₄ ⋯
          ⋯ ⋯).hom

Tactic:
· simp only [← Iso.comp_inv_eq, Category.assoc]
    exact (pageD_eq X data r hr pq' pq'' hpq' _ _ _ _ _ rfl rfl ..).symm

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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ data.i₀ r pq'' ⋯ ≤ i₀'

Tactic:
simpa using

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ data.i₀ r pq'' ⋯ ≤ data.i₁ pq''
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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ data.i₀ r pq'' ⋯ ≤ i₀'

Tactic:
simpa using

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ data.i₀ r pq'' ⋯ ≤ data.i₁ pq''
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₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ x = 0

Tactic:
rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁), hx, zero_comp]

Goal state after: