mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case right
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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p', q').2 + (-r, r - 1).2 = ↑(p, q).2

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv
⊢ n₀ = n₁ - 1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Semiprimary

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝¹ : RingHomSurjective τ₁₂
inst✝ : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Submodule.comap f (Module.jacobson R₂ M₂) ≤ f.ker

Tactic:
jacobson_eq_bot,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝¹ : RingHomSurjective τ₁₂
inst✝ : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Submodule.comap f ⊥ ≤ f.ker
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
this : h.right.opcyclesIso.hom = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ n₂ = n₁ + 1

Tactic:
lia

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'' : κ
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
h : ¬(c r).Rel pq' pq''
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₂ = data.deg pq' + 1

Tactic:
lia

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'' : κ
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''
this : data.deg pq' + 1 = data.deg pq''
⊢ n₂ = data.deg pq''

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ Function.Injective fun N ↦
    let __AddSubmonoid := N.toAddSubmonoid;
    { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }

Tactic:
intro N1

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
N1 : Submodule S M
⊢ ∀ ⦃a₂ : Submodule S M⦄,
    (fun N ↦
            let __AddSubmonoid := N.toAddSubmonoid;
            { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
          N1 =
        (fun N ↦
            let __AddSubmonoid := N.toAddSubmonoid;
            { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
          a₂ →
      N1 = a₂
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ ∀ {a b : Submodule S M},
    {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          a ≤
        {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          b ↔
      a ≤ b

Tactic:
intro N1

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
N1 : Submodule S M
⊢ ∀ {b : Submodule S M},
    {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          N1 ≤
        {
            toFun := fun N ↦
              let __AddSubmonoid := N.toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            inj' := ⋯ }
          b ↔
      N1 ≤ b
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₁ 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₂
h : (c r).Rel pq pq'
⊢ i₃ = data.i₁ pq

Tactic:
hi₃,

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

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {M : ι → Type u_6} [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)]
    [∀ (i : ι), IsArtinian R (M i)], IsArtinian R ((i : ι) → M i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Type u_6} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)) →
      ∀ {M : β → Type u_6} [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)]
        [∀ (i : β), IsArtinian R (M i)], IsArtinian R ((i : β) → M i)

R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_5 + 1} → Type u_6} [inst : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_5 + 1}) → Module R (M i)] [∀ (i : PEmpty.{u_5 + 1}), IsArtinian R (M i)],
    IsArtinian R ((i : PEmpty.{u_5 + 1}) → M i)

R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α : Type u_5} [Fintype α],
    (∀ {M : α → Type u_6} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)) →
      ∀ {M : Option α → Type u_6} [inst : (i : Option α) → AddCommGroup (M i)]
        [inst_1 : (i : Option α) → Module R (M i)] [∀ (i : Option α), IsArtinian R (M i)],
        IsArtinian R ((i : Option α) → M i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {M : ι → Submodule R P} [∀ (i : ι), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_5 + 1} → Submodule R P} [∀ (i : PEmpty.{u_5 + 1}), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α : Type u_5} [Fintype α],
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R P} [∀ (i : Option α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
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).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
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'
inst✝ : X.HasSpectralSequence data
h : ¬(c r).Rel pq pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ n₀ = data.deg pq' - 1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
h : Module.jacobson R M = ⊥
s : Finset { m // IsCoatom m }
hs : ∀ (a : { m // IsCoatom m }), s.inf Subtype.val ≤ ↑a
x✝ : ∀ (m : ↥s), IsSimpleModule R (M ⧸ ↑↑m)
f : M →ₗ[R] (m : ↥s) → M ⧸ ↑↑m := LinearMap.pi fun m ↦ (↑↑m).mkQ
x : M
hx : x ∈ f.ker
⊢ ∀ p ∈ {m | IsCoatom m}, x ∈ p

Tactic:
exact fun m hm ↦ hs ⟨m, hm⟩ <| Submodule.mem_finsetInf.mpr fun i hi ↦
        (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩

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' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
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'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃ = data.i₁ pq

Tactic:
hi₃,

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).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
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'
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.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).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
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'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
this : data.deg pq + 1 = data.deg pq'
⊢ n₀ = data.deg pq

Tactic:
lia

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' 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' (_proof_27 r₀ r r' hrr' hr)
hi₀ : i₀ = data.i₀ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₃' : i₃' = data.i₃ r' pq' (_proof_27 r₀ r r' hrr' hr)
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : autoParam (n₀ + 1 = n₁) homologyIso'._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) homologyIso'._auto_3
⊢ r₀ ≤ r'

Tactic:
lia

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' 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' (_proof_27 r₀ r r' hrr' hr)
hi₀ : i₀ = data.i₀ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₃' : i₃' = data.i₃ r' pq' (_proof_27 r₀ r r' hrr' hr)
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ r₀ ≤ r'

Tactic:
lia

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' 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' (_proof_27 r₀ r r' hrr' hr)
hi₀ : i₀ = data.i₀ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₃' : i₃' = data.i₃ r' pq' (_proof_27 r₀ r r' hrr' hr)
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
⊢ r ≤ r'

Tactic:
lia

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' 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' (_proof_27 r₀ r r' hrr' hr)
hi₀ : i₀ = data.i₀ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₃' : i₃' = data.i₃ r' pq' (_proof_27 r₀ r r' hrr' hr)
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
⊢ data.deg pq' - 1 + 1 = data.deg pq'

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsArtinianRing (R i)],
    IsArtinianRing ((i : ι) → R i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Goal state after:
ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsArtinianRing (R i)],
        IsArtinianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsArtinianRing (R i)],
        IsArtinianRing ((i : β) → R i)

ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsArtinianRing (R i)], IsArtinianRing ((i : PEmpty.{u_2 + 1}) → R i)

ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsArtinianRing (R i)],
        IsArtinianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsArtinianRing (R i)],
        IsArtinianRing ((i : Option α) → R i)
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₀
inst✝ : X.HasSpectralSequence data
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' (_proof_27 r₀ r r' hrr' hr)
hi₀ : i₀ = data.i₀ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' (_proof_28 r₀ r r' hrr' hr)
hi₃' : i₃' = data.i₃ r' pq' (_proof_27 r₀ r r' hrr' hr)
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequence_iso._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequence_iso._auto_3
⊢ r₀ ≤ r'

Tactic:
lia

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₀
inst✝ : X.HasSpectralSequence data
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₂
⊢ n₀ = n₁ - 1

Tactic:
lia

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₀
inst✝ : X.HasSpectralSequence data
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₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ n₂ = n₁ + 1

Tactic:
lia

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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ q + 1 ≤ 0

Tactic:
lia

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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
⊢ p < 0

Tactic:
lia

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₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ 0 < q

Tactic:
lia

Goal state after: