awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X)
      (NatTrans.app (Iso.hom (iso C n)) X)
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯)) (op X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) (op (op X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X)
    (NatTrans.app (Iso.hom (iso C n)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorOpIso C m n ⋯)) (op X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n m hnm)) (op (op X)))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n : ℤ
hnm : n + -n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X)
    (NatTrans.app (Iso.hom (iso C n)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯)) (op X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) (op (op X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : autoParam (n + m = 0) iso_inv_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X)
      (NatTrans.app (Iso.inv (iso C n)) X)
      (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) (op (op X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯)) (op X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X)
    (NatTrans.app (Iso.inv (iso C n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n m hnm)) (op (op X)) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorOpIso C m n ⋯)) (op X)))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n : ℤ
hnm : n + -n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X)
    (NatTrans.app (Iso.inv (iso C n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) (op (op X)) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯)) (op X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X Y : Cᵒᵖᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    op (Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) Y) ⟶
      op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X))
    (Quiver.Hom.op
      (Functor.map (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) f ≫
        Iso.hom
          ((fun (X : Cᵒᵖᵒᵖ) ↦
              (Iso.unop (Iso.unop (Iso.app (shiftFunctorOpIso Cᵒᵖ n (-n) ⋯) X)) ≪≫
                  Iso.unop (Iso.app (Iso.symm (shiftFunctorOpIso C (-n) n ⋯)) (unop X)) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X ≅
                  Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X))
            Y)))
    (Quiver.Hom.op
      (Iso.hom
          ((fun (X : Cᵒᵖᵒᵖ) ↦
              (Iso.unop (Iso.unop (Iso.app (shiftFunctorOpIso Cᵒᵖ n (-n) ⋯) X)) ≪≫
                  Iso.unop (Iso.app (Iso.symm (shiftFunctorOpIso C (-n) n ⋯)) (unop X)) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X ≅
                  Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X))
            X) ≫
        Functor.map (unopUnop C ⋙ shiftFunctor C n) f))

Tactic:
simp [shiftFunctor_op_map _ n (-n), shiftFunctor_op_map _ (-n) n]

Premises used: CategoryTheory.Pretriangulated.shiftFunctor_op_map, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) iso_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X)
      (NatTrans.app (Iso.hom (iso C n)) X)
      (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) X)) ≫
        Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯)) (unop X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (iso C n)) X)
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n m hnm)) X)) ≫
      Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C m n ⋯)) (unop X)))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (iso C n)) X)
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) X)) ≫
      Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯)) (unop X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) iso_inv_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X)
      (NatTrans.app (Iso.inv (iso C n)) X)
      (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯)) (unop X)) ≫
        Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X)
    (NatTrans.app (Iso.inv (iso C n)) X)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C m n ⋯)) (unop X)) ≫
      Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n m hnm)) X)))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X)
    (NatTrans.app (Iso.inv (iso C n)) X)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯)) (unop X)) ≫
      Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n (-n) hnm)) X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0 ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (iso C 0)) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (opOp C) ℤ)) X)

Tactic:
Quiver.Hom.unop_inj (Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
w :
  Eq.{v_1 + 1} (α :=
    unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0 ⋙ opOp C) X)) ⟶
      unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (iso C 0)) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (opOp C) ℤ)) X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0 ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (iso C 0)) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (opOp C) ℤ)) X)

Tactic:
refine Quiver.Hom.unop_inj (Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
⊢ Eq.{v_1 + 1} (α :=
    unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0 ⋙ opOp C) X)) ⟶
      unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (iso C 0)) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (opOp C) ℤ)) X)))

Tactic:
simp [iso_hom_app X 0 0, shiftFunctorZero_op_inv_app,
      shiftFunctorZero_op_hom_app]

Premises used: CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app, CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app, CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
w :
  ∀ (X : C),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (p + q) ⋙ opOp C) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (p + q)) X)
      (NatTrans.app (Iso.hom (iso C (p + q))) X)
      (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_1, u_1, u_1} C Cᵒᵖᵒᵖ) (shiftFunctor C (p + q) ⋙ opOp C)
      (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (p + q)))
    (iso C (p + q)) (Functor.CommShift.isoAdd (iso C p) (iso C q))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
X : C
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (p + q) ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (p + q)) X)
    (NatTrans.app (Iso.hom (iso C (p + q))) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)

Tactic:
Quiver.Hom.unop_inj (Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
X : C
w :
  Eq.{v_1 + 1} (α :=
    unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (p + q) ⋙ opOp C) X)) ⟶
      unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (p + q)) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (iso C (p + q))) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (p + q) ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (p + q)) X)
    (NatTrans.app (Iso.hom (iso C (p + q))) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)

Tactic:
refine Quiver.Hom.unop_inj (Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
X : C
⊢ -p + -q = -(p + q)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
X : C
⊢ Eq.{v_1 + 1} (α :=
    unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (p + q) ⋙ opOp C) X)) ⟶
      unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ (p + q)) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (iso C (p + q))) X)))
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)))

Tactic:
simp [← shiftFunctorAdd'_eq_shiftFunctorAdd, ← unop_comp_assoc, ← Functor.map_comp,
      fun X n ↦ iso_hom_app X n (-n) (add_neg_cancel n),
      shiftFunctor_op_map _ q (-q),
      shiftFunctorAdd'_op_inv_app _ p q (p + q) rfl (-p) (-q) (-(p + q))
        (add_neg_cancel p) (add_neg_cancel q) (add_neg_cancel (p + q)),
      shiftFunctorAdd'_op_hom_app _ (-p) (-q) (-(p + q)) (by lia) p q (p + q)
        (neg_add_cancel p) (neg_add_cancel q) (neg_add_cancel (p + q))]

Premises used: add_neg_cancel, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app, neg_add_cancel, HAdd.hAdd, CategoryTheory.unop_comp_assoc, CategoryTheory.Pretriangulated.shiftFunctor_op_map, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app, Neg.neg, rfl, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
w :
  ∀ (X : Cᵒᵖᵒᵖ),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0 ⋙ unopUnop C) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C (A := ℤ) 0) X)
      (NatTrans.app (Iso.hom (iso C 0)) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (unopUnop C) ℤ)) X)
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_1, u_1, u_1} Cᵒᵖᵒᵖ C) (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0 ⋙ unopUnop C)
      (unopUnop C ⋙ shiftFunctor C (A := ℤ) 0))
    (iso C 0) (Functor.CommShift.isoZero (unopUnop C) ℤ)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 0 ⋙ unopUnop C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (iso C 0)) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (unopUnop C) ℤ)) X)

Tactic:
simp [iso_hom_app _ 0 0, shiftFunctorZero_op_inv_app,
      shiftFunctorZero_op_hom_app]

Premises used: CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app, CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app, CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
w :
  ∀ (X : Cᵒᵖᵒᵖ),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (p + q) ⋙ unopUnop C) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C (p + q)) X)
      (NatTrans.app (Iso.hom (iso C (p + q))) X)
      (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_1, u_1, u_1} Cᵒᵖᵒᵖ C) (shiftFunctor Cᵒᵖᵒᵖ (p + q) ⋙ unopUnop C)
      (unopUnop C ⋙ shiftFunctor C (p + q)))
    (iso C (p + q)) (Functor.CommShift.isoAdd (iso C p) (iso C q))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
X : Cᵒᵖᵒᵖ
⊢ -p + -q = -(p + q)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : autoParam (n + m = 0) commShiftIso_opOp_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (opOp C) n)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorOpIso C m n ⋯)) (op X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n m hnm)) (op (op X)))

Tactic:
OpOpCommShift.iso_hom_app ..

Premises used: CategoryTheory.Functor.op, CategoryTheory.shiftFunctor, CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app, Int.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : autoParam (n + m = 0) commShiftIso_opOp_inv_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X)
    (NatTrans.app (Iso.inv (Functor.commShiftIso (opOp C) n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n m hnm)) (op (op X)) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorOpIso C m n ⋯)) (op X)))

Tactic:
OpOpCommShift.iso_inv_app ..

Premises used: CategoryTheory.Functor.op, CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app, CategoryTheory.shiftFunctor, Int.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) commShiftIso_unopUnop_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (unopUnop C) n)) X)
    (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ n m hnm)) X)) ≫
      Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C m n ⋯)) (unop X)))

Tactic:
UnopUnopCommShift.iso_hom_app ..

Premises used: CategoryTheory.Functor.op, CategoryTheory.shiftFunctor, CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app, Int.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) commShiftIso_unopUnop_inv_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C n) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ n ⋙ unopUnop C) X)
    (NatTrans.app (Iso.inv (Functor.commShiftIso (unopUnop C) n)) X)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C m n ⋯)) (unop X)) ≫
      Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ n m hnm)) X)))

Tactic:
UnopUnopCommShift.iso_inv_app ..

Premises used: CategoryTheory.Functor.op, CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app, CategoryTheory.shiftFunctor, Int.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
w :
  ∀ (X : C),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1}
          (shiftFunctor C n ⋙ Equivalence.inverse (opOpEquivalence C) ⋙ Equivalence.functor (opOpEquivalence C)) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C ⋙ shiftFunctor C n) X)
      (NatTrans.app
        (Iso.hom
            (Functor.commShiftIso (Equivalence.inverse (opOpEquivalence C) ⋙ Equivalence.functor (opOpEquivalence C))
              n) ≫
          Functor.whiskerRight (Iso.hom (Equivalence.counitIso (opOpEquivalence C))) (shiftFunctor C n))
        X)
      (NatTrans.app
        (Functor.whiskerLeft (shiftFunctor C n) (Iso.hom (Equivalence.counitIso (opOpEquivalence C))) ≫
          Iso.hom (Functor.commShiftIso (𝟭 C) n))
        X)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (shiftFunctor C n ⋙ Equivalence.inverse (opOpEquivalence C) ⋙ Equivalence.functor (opOpEquivalence C))
      (𝟭 C ⋙ shiftFunctor C n))
    (Iso.hom
        (Functor.commShiftIso (Equivalence.inverse (opOpEquivalence C) ⋙ Equivalence.functor (opOpEquivalence C)) n) ≫
      Functor.whiskerRight (Iso.hom (Equivalence.counitIso (opOpEquivalence C))) (shiftFunctor C n))
    (Functor.whiskerLeft (shiftFunctor C n) (Iso.hom (Equivalence.counitIso (opOpEquivalence C))) ≫
      Iso.hom (Functor.commShiftIso (𝟭 C) n))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : C
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor C n ⋙ Equivalence.inverse (opOpEquivalence C) ⋙ Equivalence.functor (opOpEquivalence C)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C ⋙ shiftFunctor C n) X)
    (NatTrans.app
      (Iso.hom
          (Functor.commShiftIso (Equivalence.inverse (opOpEquivalence C) ⋙ Equivalence.functor (opOpEquivalence C)) n) ≫
        Functor.whiskerRight (Iso.hom (Equivalence.counitIso (opOpEquivalence C))) (shiftFunctor C n))
      X)
    (NatTrans.app
      (Functor.whiskerLeft (shiftFunctor C n) (Iso.hom (Equivalence.counitIso (opOpEquivalence C))) ≫
        Iso.hom (Functor.commShiftIso (𝟭 C) n))
      X)

Tactic:
simp [Functor.commShiftIso_comp_hom_app,
          commShiftIso_opOp_hom_app _ n (-n),
          commShiftIso_unopUnop_hom_app _ n (-n),
          ← unop_comp_assoc]

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.unop_comp_assoc, CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app, Neg.neg