awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
refine_1 :
  Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).f =
    ((page X data r hr).sc' pq pq' pq'').f ≫
      Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯)
refine_2 :
  Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).g =
    ((page X data r hr).sc' pq pq' pq'').g ≫
      Iso.hom
        (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃ n₄
          ⋯ ⋯ ⋯)
⊢ (page X data r hr).sc' pq pq' pq'' ≅
    X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
      (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂ n₃
      n₄ hn₁ hn₂ hn₃ hn₄

Tactic:
refine ShortComplex.isoMk
    (pageXIso _ _ _ hr _ _ _ _ _ rfl rfl rfl rfl _ _ _ (by have := data.hc r pq pq' hpq; lia))
    (pageXIso _ _ _ hr _ _ _ _ _ (by rw [data.hc₀₂ r pq' pq'' hpq'])
    (by rw [data.hc₁₃ r pq' pq'' hpq'])
    (by rw [data.hc₀₂ r pq pq' hpq]) (by rw [data.hc₁₃ r pq pq' hpq]) _ _ _ hn₂')
    (pageXIso _ _ _ hr _ _ _ _ _ rfl rfl rfl rfl _ _ _ (by have := data.hc r pq' pq'' hpq'; lia))
    ?_ ?_

Premises used: CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
refine_1 :
  Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
            (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁
            n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).f ≫
        Iso.inv
          (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃
            hn₂' ⋯ ⋯) =
    ((page X data r hr).sc' pq pq' pq'').f
⊢ Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).f =
    ((page X data r hr).sc' pq pq' pq'').f ≫
      Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯)

Tactic:
simp only [← Iso.comp_inv_eq, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
⊢ Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
            (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁
            n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).f ≫
        Iso.inv
          (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃
            hn₂' ⋯ ⋯) =
    ((page X data r hr).sc' pq pq' pq'').f

Tactic:
(pageD_eq X data r hr pq pq' hpq _ _ _ _ _ (data.hc₀₂ r pq' pq'' hpq').symm
      (data.hc₁₃ r pq' pq'' hpq').symm ..).symm

Premises used: CategoryTheory.Abelian.SpectralObject.E, CategoryTheory.ShortComplex.Exact.desc, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂, CategoryTheory.Abelian.SpectralObject.d, dite, CategoryTheory.ShortComplex.homology, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX, CategoryTheory.Abelian.SpectralObject.descE, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, Eq.symm, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
⊢ Iso.hom (pageXIso X data r hr pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
            (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁
            n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).f ≫
        Iso.inv
          (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃
            hn₂' ⋯ ⋯) =
    ((page X data r hr).sc' pq pq' pq'').f

Tactic:
exact (pageD_eq X data r hr pq pq' hpq _ _ _ _ _ (data.hc₀₂ r pq' pq'' hpq').symm
      (data.hc₁₃ r pq' pq'' hpq').symm ..).symm

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, Eq.symm
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
refine_2 :
  Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
            (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁
            n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).g ≫
        Iso.inv
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃
            n₄ ⋯ ⋯ ⋯) =
    ((page X data r hr).sc' pq pq' pq'').g
⊢ Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
          (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁ n₂
          n₃ n₄ hn₁ hn₂ hn₃ hn₄).g =
    ((page X data r hr).sc' pq pq' pq'').g ≫
      Iso.hom
        (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃ n₄
          ⋯ ⋯ ⋯)

Tactic:
simp only [← Iso.comp_inv_eq, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
⊢ Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
            (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁
            n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).g ≫
        Iso.inv
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃
            n₄ ⋯ ⋯ ⋯) =
    ((page X data r hr).sc' pq pq' pq'').g

Tactic:
(pageD_eq X data r hr pq' pq'' hpq' _ _ _ _ _ rfl rfl ..).symm

Premises used: CategoryTheory.Abelian.SpectralObject.E, CategoryTheory.ShortComplex.Exact.desc, CategoryTheory.Abelian.SpectralObject.d, dite, CategoryTheory.ShortComplex.homology, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX, CategoryTheory.Abelian.SpectralObject.descE, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, Eq.symm, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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'
⊢ Iso.hom
        (pageXIso X data r hr pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ n₁ n₂ n₃ hn₂'
          ⋯ ⋯) ≫
      (X.dShortComplex (i₀ := data.i₀ r pq'' ⋯) (i₇ := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
            (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) n₀ n₁
            n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).g ≫
        Iso.inv
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯ n₂ n₃
            n₄ ⋯ ⋯ ⋯) =
    ((page X data r hr).sc' pq pq' pq'').g

Tactic:
exact (pageD_eq X data r hr pq' pq'' hpq' _ _ _ _ _ rfl rfl ..).symm

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, Eq.symm, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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₂
pos :
  ∀ (h : (c r).Rel pq' pq''),
    Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
      ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
            (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
          (page X data r hr).d pq' pq'' :
        X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
      (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
neg :
  ∀ (h : ¬(c r).Rel pq' pq''),
    Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
      ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
            (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
          (page X data r hr).d pq' pq'' :
        X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
      (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
⊢ Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
          (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
        (page X data r hr).d pq' pq'' :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')

Tactic:
by_cases h : (c r).Rel pq' pq''

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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''
pos :
  Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ pageX X data r pq'' ⋯)
    ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
          (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
        pageD X data r pq' pq'' ⋯ :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ pageX X data r pq'' ⋯)
    (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
⊢ Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
          (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
        (page X data r hr).d pq' pq'' :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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 only [hi₀', data.i₀_prev r r' _ _ h] using data.le₀₁ r pq''

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_prev
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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''
rw : data.i₀ r' pq' ⋯ = data.i₁ pq''
rw₁ rw₂ : data.i₁ pq'' = data.i₁ pq''
⊢ i₀' = data.i₁ pq''

Tactic:
rw [hi₀', data.i₀_prev r r' pq' pq'' h]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_prev
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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''
neg :
  Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
          (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
        0 :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
neg₁ neg₂ : Eq.{v_1 + 1} (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'') 0 0
⊢ Eq (α := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    ((X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
          (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
        (page X data r hr).d pq' pq'' :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')
    (0 : X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ (page X data r hr).X pq'')

Tactic:
rw [HomologicalComplex.shape _ _ _ h, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
dsimp :
  Mono (X := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ ⋯)
    (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ ⋯ ≫
        Iso.inv (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ ⋯) :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ ⋯ ⟶ pageX X data r pq' hr)
⊢ Mono (kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).f

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ ⋯)
    (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ ⋯ ≫
        Iso.inv (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ ⋯) :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ ⋯ ⟶ pageX X data r pq' hr)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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_3 : X.HasSpectralSequence data
h : ¬(c r).Rel pq' pq''
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
apply : IsZero.{v_1, u_1} ((X.H n₂).obj (mk₁ (homOfLE ⋯)))
⊢ IsIso (X := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂) (Y :=
    X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
    (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶
        X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
apply X.isIso_map_fourδ₁Toδ₀_of_isZero ..

Premises used: CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero
-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} 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_3 : X.HasSpectralSequence data
h : ¬(c r).Rel pq' pq''
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₂ = data.deg pq' + 1

Tactic:
lia