awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : n + 1 = n'
⊢ ((X.spectralSequence data).page r₀ ⋯).d pq pq' =
    Iso.hom (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn) ≫
      X.δ (homOfLE ⋯) (homOfLE ⋯) n n' hn' ≫ Iso.inv (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯)

Tactic:
simpa [X.spectralSequenceFirstPageXIso_hom data pq j k hj hk (n - 1) n n',
    ← X.d_EIsoH_hom_assoc _ _ (n - 1) n n' (n' + 1),
    X.spectralSequenceFirstPageXIso_inv data pq' i j hi _ _ n' _ _ hn' _]
    using spectralSequence_page_d_eq _ _ _ _ _ _ hpq ..

Premises used: CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq, HSub.hSub, CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom_assoc, HAdd.hAdd, CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv, OfNat.ofNat, CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : Type u_2
κ : Type u_3
inst : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
pq : κ
hrr' : r + 1 = r'
hr : r₀ ≤ r
⊢ data.i₀ r' pq ⋯ ≤ data.i₀ r pq ⋯

Tactic:
data.antitone_i₀ r r' pq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.antitone_i₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : Type u_2
κ : Type u_3
inst : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
pq : κ
hrr' : r + 1 = r'
hr : r₀ ≤ r
⊢ data.i₃ r pq ⋯ ≤ data.i₃ r' pq ⋯

Tactic:
data.monotone_i₃ r r' pq

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.monotone_i₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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' ⋯
rw : data.i₀ r' pq' ⋯ ≤ data.i₀ r pq' ⋯
⊢ i₀' ≤ i₀

Tactic:
rw [hi₀', hi₀]
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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' ⋯

Tactic:
data.antitone_i₀ r r' pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.antitone_i₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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' ⋯

Tactic:
exact data.antitone_i₀ r r' pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.antitone_i₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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'
⊢ data.i₀ r pq' ⋯ ≤ data.i₁ pq'

Tactic:
have := data.le₀₁ r pq'
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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 only [hi₀, hi₁] using data.le₀₁ r pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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 only [hi₁, hi₂] using data.le₁₂ pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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 only [hi₂, hi₃] using data.le₂₃ r pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Goal:
ι : 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 only [hi₃, hi₃'] using data.monotone_i₃ r r' pq'

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.monotone_i₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
simp : pq.2 - r + 2 ≤ pq.2
⊢ WithBotTop.coe (pq.2 - r + 2) ≤ WithBotTop.coe pq.2

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
⊢ pq.2 - r + 2 ≤ pq.2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
pq : ℤ × ℤ
⊢ WithBotTop.coe pq.2 ≤ WithBotTop.coe (pq.2 + 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
simp : pq.2 + 1 ≤ pq.2 + r - 1
⊢ WithBotTop.coe (pq.2 + 1) ≤ WithBotTop.coe (pq.2 + r - 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
⊢ pq.2 + 1 ≤ pq.2 + r - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_7
dsimp : pq.1 + pq.2 + 1 = pq.1 + r + (pq.2 + (1 - r))
⊢ pq.1 + pq.2 + 1 = (pq + (r, 1 - r)).1 + (pq + (r, 1 - r)).2

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_7
⊢ pq.1 + pq.2 + 1 = pq.1 + r + (pq.2 + (1 - r))

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_8
⊢ WithBotTop.coe (pq.2 - r + 2) = WithBotTop.coe (pq.2 + (1 - r) + 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℤ × ℤ
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_9
⊢ WithBotTop.coe pq.2 = WithBotTop.coe (pq.2 + (1 - r) + r - 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' simp : r ≤ r'
⊢ WithBotTop.coe (pq.2 - r' + 2) ≤ WithBotTop.coe (pq.2 - r + 2)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ r'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℤ × ℤ
hr : 2 ≤ r
hrr' simp : r ≤ r'
⊢ WithBotTop.coe (pq.2 + r - 1) ≤ WithBotTop.coe (pq.2 + r' - 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
hr : ℤ × ℤ
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_20
hr_1 : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_21
⊢ WithBotTop.coe (hr.2 - r' + 2) = WithBotTop.coe (hr.2 + (1 - r))

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
hr : ℤ × ℤ
hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_22
hr_1 : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_23
⊢ WithBotTop.coe (hr.2 + (1 - r) + r' - 1) = WithBotTop.coe (hr.2 + 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
simp : (↑pq.2 : ℤ) - r + 2 ≤ (↑pq.2 : ℤ)
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r + 2) ≤ WithBotTop.coe (↑pq.2 : ℤ)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ (↑pq.2 : ℤ) - r + 2 ≤ (↑pq.2 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
pq : ℕ × ℕ
⊢ WithBotTop.coe (↑pq.2 : ℤ) ≤ WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
simp : HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1 ≤ (↑pq.2 : ℤ) + r - 1
⊢ WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1) ≤ WithBotTop.coe ((↑pq.2 : ℤ) + r - 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
⊢ HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1 ≤ (↑pq.2 : ℤ) + r - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq pq' : ℕ × ℕ
hpq : (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq pq'
hr : 2 ≤ r
⊢ (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)

Tactic:
simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq

Premises used: ComplexShape.spectralSequenceNat_rel_iff
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑pq.1 : ℤ) (↑pq.2 : ℤ) + 1 = HAdd.hAdd (α := ℤ) (↑pq'.1 : ℤ) (↑pq'.2 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r + 2) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq'.2 : ℤ) 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe (↑pq.2 : ℤ) = WithBotTop.coe ((↑pq'.2 : ℤ) + r - 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' simp : r ≤ r'
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r' + 2) ≤ WithBotTop.coe ((↑pq.2 : ℤ) - r + 2)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' : r ≤ r'
⊢ r ≤ r'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq : ℕ × ℕ
hr : 2 ≤ r
hrr' simp : r ≤ r'
⊢ WithBotTop.coe ((↑pq.2 : ℤ) + r - 1) ≤ WithBotTop.coe ((↑pq.2 : ℤ) + r' - 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq pq' : ℕ × ℕ
hpq : (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq pq'
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)

Tactic:
simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq

Premises used: ComplexShape.spectralSequenceNat_rel_iff
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe ((↑pq.2 : ℤ) - r' + 2) = WithBotTop.coe (↑pq'.2 : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : (↑pq.1 : ℤ) + r = (↑pq'.1 : ℤ) ∧ (↑pq.2 : ℤ) + (1 - r) = (↑pq'.2 : ℤ)
⊢ WithBotTop.coe ((↑pq'.2 : ℤ) + r' - 1) = WithBotTop.coe (HAdd.hAdd (α := ℤ) (↑pq.2 : ℤ) 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r : ℤ
pq : ℤ × Fin l
hr : 2 ≤ r
⊢ ((↑(↑pq.2 : ℕ) : ℤ) - (r - 2)).toNat < l + 1

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r p : ℤ
q : ℕ
hq : q < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_3
simp : (↑q : ℤ) - (r - 2) ≤ (↑q : ℤ)
⊢ (⟨((↑(↑(p, (⟨q, hq⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat, ⋯⟩ : Fin (l + 1)) ≤ (p, (⟨q, hq⟩ : Fin l)).2.castSucc

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r p : ℤ
q : ℕ
hq : q < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_3
⊢ (↑q : ℤ) - (r - 2) ≤ (↑q : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
pq : ℤ × Fin l
⊢ pq.2.castSucc ≤ pq.2.succ

Tactic:
simp [Fin.le_iff_val_le_val]

Premises used: Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r : ℤ
pq : ℤ × Fin l
hr : 2 ≤ r
simp : (↑pq.2 : ℕ) + 1 ≤ ((↑(↑pq.2 : ℕ) : ℤ) + (r - 1)).toNat ∧ (↑pq.2 : ℕ) + 1 ≤ l
⊢ pq.2.succ ≤ Fin.clamp ((↑(↑pq.2 : ℕ) : ℤ) + (r - 1)).toNat l

Tactic:
simp only [Fin.le_iff_val_le_val, Fin.val_succ, le_min_iff, Fin.clamp]

Premises used: Fin.clamp, Fin.val_succ, le_min_iff, Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r : ℤ
pq : ℤ × Fin l
hr : 2 ≤ r
⊢ (↑pq.2 : ℕ) + 1 ≤ ((↑(↑pq.2 : ℕ) : ℤ) + (r - 1)).toNat ∧ (↑pq.2 : ℕ) + 1 ≤ l

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
x : ℤ
x_1 x_2 : ℤ × Fin l
h : (ComplexShape.spectralSequenceFin l (x, 1 - x)).Rel x_1 x_2
h₁ : x_1.1 + (x, 1 - x).1 = x_2.1
h₂ : (↑(↑x_1.2 : ℕ) : ℤ) + (x, 1 - x).2 = (↑(↑x_2.2 : ℕ) : ℤ)
⊢ ∀ (hr : autoParam (2 ≤ x) SpectralSequenceDataCore._auto_7),
    x_1.1 + (↑(↑x_1.2 : ℕ) : ℤ) + 1 = x_2.1 + (↑(↑x_2.2 : ℕ) : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r a₁ : ℤ
a₂ : ℕ
isLt : a₂ < l
b₁ : ℤ
b₂ : ℕ
isLt_1 : b₂ < l
h₁ : (a₁, (⟨a₂, isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b₁, (⟨b₂, isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_8
⊢ (⟨((↑(↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat, ⋯⟩ : Fin (l + 1)) =
    (b₁, (⟨b₂, isLt_1⟩ : Fin l)).2.succ

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r a₁ : ℤ
a₂ : ℕ
isLt : a₂ < l
b₁ : ℤ
b₂ : ℕ
isLt_1 : b₂ < l
h₁ : (a₁, (⟨a₂, isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b₁, (⟨b₂, isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_9
rw :
  (↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2.castSucc : ℕ) =
    (↑(Fin.clamp ((↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l) : ℕ)
⊢ (a₁, (⟨a₂, isLt⟩ : Fin l)).2.castSucc = Fin.clamp ((↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l

Tactic:
rw [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r a₁ : ℤ
a₂ : ℕ
isLt : a₂ < l
b₁ : ℤ
b₂ : ℕ
isLt_1 : b₂ < l
h₁ : (a₁, (⟨a₂, isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b₁, (⟨b₂, isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_9
dsimp : a₂ = min ((↑b₂ : ℤ) + (r - 1)).toNat l
⊢ (↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2.castSucc : ℕ) =
    (↑(Fin.clamp ((↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat l) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r a₁ : ℤ
a₂ : ℕ
isLt : a₂ < l
b₁ : ℤ
b₂ : ℕ
isLt_1 : b₂ < l
h₁ : (a₁, (⟨a₂, isLt⟩ : Fin l)).1 + (r, 1 - r).1 = (b₁, (⟨b₂, isLt_1⟩ : Fin l)).1
h₂ : (↑(↑(a₁, (⟨a₂, isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r, 1 - r).2 = (↑(↑(b₁, (⟨b₂, isLt_1⟩ : Fin l)).2 : ℕ) : ℤ)
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_9
⊢ a₂ = min ((↑b₂ : ℤ) + (r - 1)).toNat l

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_11
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_12
rw :
  ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat ≤
    ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat
⊢ (⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat, ⋯⟩ : Fin (l + 1)) ≤
    ⟨((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat, ⋯⟩

Tactic:
rw [Fin.mk_le_mk]

Premises used: Fin.mk_le_mk
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_11
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_12
⊢ ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r' - 2)).toNat ≤
    ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) - (r - 2)).toNat

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_15
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_16
⊢ ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r - 1)).toNat ≤
    ((↑(↑(a, (⟨a', isLt⟩ : Fin l)).2 : ℕ) : ℤ) + (r' - 1)).toNat

Tactic:
lia