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

Goal state before:
pp: case h₀
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) ≫
      biprod.fst =
    0 ≫ biprod.fst

pp: case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) ≫
      biprod.snd =
    0 ≫ biprod.snd

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) ≫
      biprod.fst =
    0 ≫ biprod.fst

case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)) ≫
      biprod.snd =
    0 ≫ biprod.snd
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case h₀
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁) ⊞ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₂ ≫ y₂ = y₁ ≫ biprod.desc ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)
⊢ y₁ ≫ biprod.fst = ((y₁ ≫ biprod.fst) ≫ biprod.inl + (y₁ ≫ biprod.snd) ≫ biprod.inr) ≫ biprod.fst

pp: case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁) ⊞ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₂ ≫ y₂ = y₁ ≫ biprod.desc ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)
⊢ y₁ ≫ biprod.snd = ((y₁ ≫ biprod.fst) ≫ biprod.inl + (y₁ ≫ biprod.snd) ≫ biprod.inr) ≫ biprod.snd

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁) ⊞ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₂ ≫ y₂ = y₁ ≫ biprod.desc ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)
⊢ y₁ ≫ biprod.fst = ((y₁ ≫ biprod.fst) ≫ biprod.inl + (y₁ ≫ biprod.snd) ≫ biprod.inr) ≫ biprod.fst

case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
y₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁) ⊞ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₂ ≫ y₂ = y₁ ≫ biprod.desc ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)
⊢ y₁ ≫ biprod.snd = ((y₁ ≫ biprod.fst) ≫ biprod.inl + (y₁ ≫ biprod.snd) ≫ biprod.inr) ≫ biprod.snd
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: case left
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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p, q).1 + (r, 1 - r).1 = ↑(p', q').1

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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p, q).2 + (r, 1 - r).2 = ↑(p', q').2

Tactic:
<;>

Goal state after:
case left
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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p, q).1 + (r, 1 - r).1 = ↑(p', q').1

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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p, q).2 + (r, 1 - r).2 = ↑(p', q').2
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : 0 < ↑q - r + 2
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) (p', q')

Tactic:
by constructor <;> 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 : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
hn₂ : data.deg pq + 1 = data.deg pq + 1
hn₃ : data.deg pq + 1 + 1 = data.deg pq + 2
⊢ (if hpq : (c r).Rel pq pq' then
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1)
          (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
        eqToHom ⋯
    else 0) =
    𝟙 (pageX X data r pq ⋯) ≫
      X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) hn₁ hn₂ hn₃ ≫ eqToHom ⋯

Tactic:
rw [dif_pos hpq, Category.id_comp]

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
hn₂ : data.deg pq + 1 = data.deg pq + 1
hn₃ : data.deg pq + 1 + 1 = data.deg pq + 2
⊢ X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1)
        (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
      eqToHom ⋯ =
    X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) hn₁ hn₂ hn₃ ≫ eqToHom ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

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

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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').2 + (r, 1 - r).2 = ↑(p, q).2

Tactic:
<;>

Goal state after:
case left
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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').1 + (r, 1 - r).1 = ↑(p, q).1

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.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').2 + (r, 1 - r).2 = ↑(p, q).2
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p', q') (p, q)

Tactic:
by constructor <;> lia

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

Goal state before:
pp: case left
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 (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).1 + (-r, r - 1).1 = ↑(p', q').1

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 (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).2 + (-r, r - 1).2 = ↑(p', q').2

Tactic:
<;>

Goal state after:
case left
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 (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).1 + (-r, r - 1).1 = ↑(p', q').1

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 (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).2 + (-r, r - 1).2 = ↑(p', q').2
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) (p', q')

Tactic:
by constructor <;> lia

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

Goal state before:
pp: case left
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').1 + (-r, r - 1).1 = ↑(p, q).1

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:
<;>

Goal state after:
case left
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').1 + (-r, r - 1).1 = ↑(p, q).1

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
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
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'
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p', q') (p, q)

Tactic:
by constructor <;> lia

Goal state after:
Module: Mathlib.Order.Filter.Subsingleton

Goal state before:
pp: case refine_2.inl
α : Type u_1
⊢ ⊥.Subsingleton

pp: case refine_2.inr
α : Type u_1
a : α
⊢ (pure a).Subsingleton

Tactic:
<;>

Goal state after:
case refine_2.inl
α : Type u_1
⊢ ⊥.Subsingleton

case refine_2.inr
α : Type u_1
a : α
⊢ (pure a).Subsingleton
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : One β
s : Set α
⊢ EventuallyConst (s.mulIndicator fun x ↦ 1) l ↔ 1 = 1 ∨ EventuallyConst s l

pp: case inr
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
⊢ EventuallyConst (s.mulIndicator fun x ↦ c) l ↔ c = 1 ∨ EventuallyConst s l

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : One β
s : Set α
⊢ EventuallyConst (s.mulIndicator fun x ↦ 1) l ↔ 1 = 1 ∨ EventuallyConst s l

case inr
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
⊢ EventuallyConst (s.mulIndicator fun x ↦ c) l ↔ c = 1 ∨ EventuallyConst s l
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case e'_2
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

pp: case e'_3
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)

Tactic:
<;>

Goal state after:
case e'_2
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

case e'_3
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)
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:
rw [hi₃, data.hc₁₃ r _ _ h]

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:
rw [hi₃, data.hc₁₃ r _ _ h]

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsFaithful R L M
x : L
⊢ (toEnd R L M) x = 0 ↔ x = 0

Tactic:
rw [← (toEnd R L M).toLinearMap.map_zero]
  exact toEnd_eq_iff R L M

Goal state after: