awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : 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_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X'.H n₀).obj (mk₁ (homOfLE hi₃₄)))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)

Tactic:
X'.isIso_map_fourδ₄Toδ₃_of_isZero (h := h) ..

Premises used: CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : 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_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X'.H n₀).obj (mk₁ (homOfLE hi₃₄)))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv =
    𝟙 (X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
(X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).hom_inv_id

Premises used: CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃', CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Abelian.SpectralObject.map, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : 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_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X'.H n₀).obj (mk₁ (homOfLE hi₃₄)))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv ≫
      X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ =
    𝟙 (X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
(X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃', CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Abelian.SpectralObject.map, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : 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_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h₁ : IsIso ((X'.H n₁).map (twoδ₁Toδ₀' i₁ i₂ i₃ hi₁₂ hi₂₃))
h₂ : IsIso ((X'.H n₂).map (twoδ₂Toδ₁' i₀ i₁ i₂ hi₀₁ hi₁₂))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X :=
    (X'.H n₀).obj
      (Functor.obj (functorArrows ι' 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3)
        (mk₃ { down := { down := hi₀₁ : PLift (i₀ ≤ i₁) } : ULift.{u_3, 0} (PLift (i₀ ≤ i₁)) }
          { down := { down := ⋯ : PLift (i₁ ≤ i₃) } : ULift.{u_3, 0} (PLift (i₁ ≤ i₃)) } (homOfLE hi₃₄))))
    ((X'.H n₀).map
      (Functor.map (functorArrows ι' 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3)
        (fourδ₂Toδ₁' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄)))

Tactic:
(inferInstanceAs (IsIso ((X'.H n₀).map (𝟙 _))))

Premises used: _private.0.CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁'._proof_1
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : 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_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h₁ : IsIso ((X'.H n₁).map (twoδ₁Toδ₀' i₁ i₂ i₃ hi₁₂ hi₂₃))
h₂ : IsIso ((X'.H n₂).map (twoδ₂Toδ₁' i₀ i₁ i₂ hi₀₁ hi₁₂))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X :=
    (X'.H n₀).obj
      (Functor.obj (functorArrows ι' 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3)
        (mk₃ { down := { down := hi₀₁ : PLift (i₀ ≤ i₁) } : ULift.{u_3, 0} (PLift (i₀ ≤ i₁)) }
          { down := { down := ⋯ : PLift (i₁ ≤ i₃) } : ULift.{u_3, 0} (PLift (i₁ ≤ i₃)) } (homOfLE hi₃₄))))
    ((X'.H n₀).map
      (Functor.map (functorArrows ι' 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3)
        (fourδ₂Toδ₁' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄)))

Tactic:
exact (inferInstanceAs (IsIso ((X'.H n₀).map (𝟙 _))))
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{?u.883, u_1} C
inst_1 : Abelian C
inst_2 : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℤ × ℤ
⊢ WithBotTop.coe (pq.2 - 2 + 2) = WithBotTop.coe pq.2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{?u.883, u_1} C
inst_1 : Abelian C
inst_2 : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℤ × ℤ
⊢ WithBotTop.coe (pq.2 + 1) = WithBotTop.coe (pq.2 + 2 - 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{?u.1403, u_1} C
inst_1 : Abelian C
inst_2 : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (HSub.hSub (α := ℤ) (↑pq.2 : ℤ) 2 + 2) = WithBotTop.coe (↑pq.2 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{?u.1403, u_1} C
inst_1 : Abelian C
inst_2 : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 2 - 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{?u.1988, u_1} C
inst_1 : Abelian C
inst_2 : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (HSub.hSub (α := ℤ) (-(↑pq.2 : ℤ)) 2 + 2) = WithBotTop.coe (-(↑pq.2 : ℤ))

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{?u.1988, u_1} C
inst_1 : Abelian C
inst_2 : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
pq : ℕ × ℕ
⊢ WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 1) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (-(↑pq.2 : ℤ)) 2 - 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
⊢ r₀ ≤ r₀

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
rw : data.i₁ pq = data.i₀ r₀ pq ⋯
rw₁ rw₂ : data.i₀ r₀ pq ⋯ = data.i₀ r₀ pq ⋯
⊢ i₁ = data.i₀ r₀ pq ⋯

Tactic:
rw [hi₁, ← data.hi₀₁]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₀₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
rw : data.i₂ pq = data.i₃ r₀ pq ⋯
rw₁ rw₂ : data.i₃ r₀ pq ⋯ = data.i₃ r₀ pq ⋯
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
rw [hi₂, data.hi₂₃]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₂₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
⊢ r₀ ≤ r₀

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
rw : data.i₁ pq = data.i₀ r₀ pq ⋯
rw₁ rw₂ : data.i₀ r₀ pq ⋯ = data.i₀ r₀ pq ⋯
⊢ i₁ = data.i₀ r₀ pq ⋯

Tactic:
rw [hi₁, ← data.hi₀₁]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₀₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_2
rw : data.i₂ pq = data.i₃ r₀ pq ⋯
rw₁ rw₂ : data.i₃ r₀ pq ⋯ = data.i₃ r₀ pq ⋯
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
rw [hi₂, data.hi₂₃]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₂₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₀ = n₁ - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
obtain :
  ∀ (hn₁ : n₁ - 1 + 1 = n₁),
    Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
      (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
      (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯) ≫
        (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).hom)
⊢ Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
      (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom)

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
obtain :
  Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯) ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ (n₁ + 1) hn₁ ⋯).hom)
⊢ Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯) ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).hom)

Tactic:
obtain rfl := hn₂

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₁ - 1 + 1 = n₁
⊢ Eq (α := ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ (X.H n₁).obj (mk₁ (homOfLE ⋯)))
    (Iso.hom (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    (Iso.hom (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯) ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ (n₁ + 1) hn₁ ⋯).hom)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
⊢ r₀ ≤ r₀

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
rw : data.i₁ pq = data.i₀ r₀ pq ⋯
rw₁ rw₂ : data.i₀ r₀ pq ⋯ = data.i₀ r₀ pq ⋯
⊢ i₁ = data.i₀ r₀ pq ⋯

Tactic:
rw [hi₁, ← data.hi₀₁]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₀₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_2
rw : data.i₂ pq = data.i₃ r₀ pq ⋯
rw₁ rw₂ : data.i₃ r₀ pq ⋯ = data.i₃ r₀ pq ⋯
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
rw [hi₂, data.hi₂₃]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₂₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
obtain :
  ∀ (hn₁ : n₁ - 1 + 1 = n₁),
    Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
      (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
      ((X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv ≫
        Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯))
⊢ Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯))

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
obtain :
  Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ (n₁ + 1) hn₁ ⋯).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯))
⊢ Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯))

Tactic:
obtain rfl := hn₂

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₁ - 1 + 1 = n₁
⊢ Eq (α := (X.H n₁).obj (mk₁ (homOfLE ⋯)) ⟶ ((X.spectralSequence data).page r₀ ⋯).X pq)
    (Iso.inv (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁'))
    ((X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ (n₁ + 1) hn₁ ⋯).inv ≫
      Iso.inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : 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 only [hi, hj, data.hc₁₃ r₀ pq pq' hpq, ← data.hi₂₃ pq']
            using data.le₁₂ pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₂₃, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : 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 only [hj, hk] using data.le₁₂ pq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : 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
rw : data.i₁ pq = data.i₂ pq'
rw₁ : data.i₁ pq = data.i₀ r₀ pq ⋯
rw₂ rw₃ : data.i₁ pq = data.i₁ pq
⊢ j = data.i₂ pq'

Tactic:
rw [hj, ← data.hc₀₂ r₀ pq pq' hpq, data.hi₀₁ pq]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₀₁, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Abelian.{u_4, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, u_4, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst_3 : data.HasFirstPageComputation
inst_4 : 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
rw : n + 1 = data.deg pq'
rw₁ : data.deg pq + 1 = data.deg pq'
rw₂ rw₃ : data.deg pq' = data.deg pq'
⊢ n' = data.deg pq'

Tactic:
rw [← hn', hn, data.hc r₀ pq pq' hpq]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc