mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ ((lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
          (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
            (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      ((lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
          (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
            (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
        F.map ((shiftFunctorAdd C a b).hom.app X) ≫
          (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
            (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      ((lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
          (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
            (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
        F.map ((shiftFunctorAdd C a b).hom.app X) ≫
          (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
            (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
        ((lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
            (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
          F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
        ((lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
            (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
          F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
        (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
          (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X)) ≫
            F.map ((shiftFunctorAdd C a b).hom.app X) ≫
              (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
                (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                  (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
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' a : ℤ
γ₁ γ₂ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn

Tactic:
by
  change (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _
  apply map_add

Goal state after:
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
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L).d (p + n') q +
      m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + m) ⋯).inv =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv

Tactic:
simp only [shiftFunctorObjXIso, shiftFunctor_obj_d',
      Linear.comp_units_smul, assoc, HomologicalComplex.XIsoOfEq_inv_comp_d,
      add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add,
      add_right_inj, smul_smul]

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
⊢ m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (HomologicalComplex.XIsoOfEq L ⋯).inv =
    (a.negOnePow * m.negOnePow) • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (HomologicalComplex.XIsoOfEq L ⋯).inv
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ ((T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁)) ≫
      piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    ((Pi.lift fun j ↦ (φ j).hom₃) ≫
        (Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
      piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    ((Pi.lift fun j ↦ (φ j).hom₃) ≫
        (Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
      piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    ((Pi.lift fun j ↦ (φ j).hom₃) ≫
        (Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
      piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫
      ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
        piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫
      ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
        piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ (T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫
      (Limits.Pi.map fun j ↦ (T j).mor₃) ≫
        inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁
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 = a.negOnePow • rightShift 0 a m' hm'

Tactic:
rightShift_zero,

Goal state after:
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 = a.negOnePow • 0
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
      (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) =
    0

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ (Limits.Pi.map fun j ↦ (T j).mor₃) ≫
      inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
        (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) =
    0
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ (((Limits.Pi.map fun j ↦ (T j).mor₃) ≫
        inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
          (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁)) ≫
      piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) =
    0

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫
      (inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
          (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁)) ≫
        piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) =
    0
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₃ ≫
          (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.hom₁)) ≫
        (shiftFunctorComm C 1 n).hom.app Y✝.obj₁

Tactic:
assoc,

Goal state after:
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₃ ≫
          (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.hom₁)) ≫
        (shiftFunctorComm C 1 n).hom.app Y✝.obj₁
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₃ ≫
          (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.hom₁)) ≫
        (shiftFunctorComm C 1 n).hom.app Y✝.obj₁

Tactic:
assoc,

Goal state after:
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₃ ≫
        (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.hom₁) ≫
          (shiftFunctorComm C 1 n).hom.app Y✝.obj₁
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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C b).map
            ((CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)

Tactic:
assoc,

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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C b).map
            ((CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)
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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        ((CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₃) ≫
            (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:
assoc,

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.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₃) ≫
          (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₁)