mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯) ≫
        L.d (p + n') q +
      m'.negOnePow •
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).d p (p + 1) ≫
          ((a * n' + a * (a - 1) / 2).negOnePow •
            (K.shiftFunctorObjXIso a (p + 1) (p + 1 + a) ⋯).hom ≫ γ.v (p + 1 + a) q ⋯) =
    a.negOnePow •
      (a * m' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫
          (γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q + m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯)

Tactic:
]

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯) ≫
        L.d (p + n') q +
      m'.negOnePow •
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).d p (p + 1) ≫
          ((a * n' + a * (a - 1) / 2).negOnePow •
            (K.shiftFunctorObjXIso a (p + 1) (p + 1 + a) ⋯).hom ≫ γ.v (p + 1 + a) q ⋯) =
    a.negOnePow •
      (a * m' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫
          (γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q + m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ n.negOnePow •
      (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫
        (shiftFunctorComm C 1 n).hom.app X✝.obj₁ ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    n.negOnePow •
      (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫
        (shiftFunctorComm C 1 n).hom.app X✝.obj₁ ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a + a * n' + a * (a - 1) / 2).negOnePow

Tactic:
]

Goal state after:
case pos.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a + a * n' + a * (a - 1) / 2).negOnePow
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫
        (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁ ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) ≫
          (CategoryTheory.shiftFunctor C b).map ((shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
            (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫
        (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁ ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) ≫
          (CategoryTheory.shiftFunctor C b).map ((shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
            (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯ =
    a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : (shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : (shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : ¬n + 1 = m
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯ =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₁ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (eqToHom ⋯).hom₁ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁)

Tactic:
]

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₁ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (eqToHom ⋯).hom₁ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₂ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂) =
    (eqToHom ⋯).hom₂ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂)

Tactic:
]

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₂ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂) =
    (eqToHom ⋯).hom₂ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯ =
    (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃ =
    (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃ =
    (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₃ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃) =
    (eqToHom ⋯).hom₃ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃)

Tactic:
]

Goal state after:
case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₃ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃) =
    (eqToHom ⋯).hom₃ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₃ = 0
⊢ ∀ (R : C) (g : T.obj₃ ⟶ R), T.mor₂ ≫ g = 0 → g = 0

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₃ = 0
⊢ ∀ (R : C) (g : T.obj₃ ⟶ R), T.mor₂ ≫ g = 0 → g = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₃ = 0
X : C
f : (CategoryTheory.shiftFunctor C 1).obj T.obj₁ ⟶ X
hg : T.mor₂ ≫ T.mor₃ ≫ f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
a✝ : Epi T.mor₂
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₃ = u₁₃

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁
⊢ T.mor₂ = 0 ↔ T.mor₂ = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0 ↔ Epi T.mor₃
⊢ T.mor₁ = 0 ↔ -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0

Tactic:
neg_eq_zero

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0 ↔ Epi T.mor₃
⊢ T.mor₁ = 0 ↔ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0 ↔ Epi T.mor₃
⊢ T.mor₁ = 0 ↔ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0 ↔ Epi T.mor₃
⊢ T.mor₁ = 0 ↔ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₁ = 0
⊢ ∀ (P : C) (g : P ⟶ T.obj₂), g ≫ T.mor₂ = 0 → g = 0

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₁ = 0
⊢ ∀ (P : C) (g : P ⟶ T.obj₂), g ≫ T.mor₂ = 0 → g = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₁ = 0
X : C
f : X ⟶ T.obj₁
hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
a✝ : Mono T.mor₂
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ v₂₃ = v₂₃

Tactic:
]

Goal state after: