awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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}
        (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) hnm)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
          X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
      (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
      (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) hnm))
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) hnm)) (Opposite.unop X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n m hnm)) (Opposite.unop X)))

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

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) hnm)) (Opposite.unop X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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} (𝟭 Cᵒᵖ) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) hnm)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) hnm))
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
    (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n m hnm)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C n m hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))))

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

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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} (𝟭 Cᵒᵖ) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
    (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) hnm)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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.{v_1 + 1} (α :=
    X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) Y)
    (f ≫ NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) X)
      (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
      (Quiver.Hom.op (Functor.map (shiftFunctor C n) (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ n) f)))))

Tactic:
(opShiftFunctorEquivalence C n).unitIso.hom.naturality f

Premises used: CategoryTheory.Equivalence.unitIso, Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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 (α :=
    Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Y)
    (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y))))
        (Quiver.Hom.op (Functor.map (shiftFunctor C n) (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ n) f))))
        (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y) :
      Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Y)
    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X ≫ f :
      Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
          X ⟶
        Y)

Tactic:
(opShiftFunctorEquivalence C n).unitIso.inv.naturality f

Premises used: CategoryTheory.Equivalence.unitIso, Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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 (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Y)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop Y))))
        (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op (Functor.map (shiftFunctor C n) f.unop)))
        (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) Y) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Y)
    (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X ≫ f :
      Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
          X ⟶
        Y)

Tactic:
(opShiftFunctorEquivalence C n).counitIso.hom.naturality f

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
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.{v_1 + 1} (α :=
    X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) Y)
    (f ≫ NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) Y)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
      (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op (Functor.map (shiftFunctor C n) f.unop))))

Tactic:
(opShiftFunctorEquivalence C n).counitIso.inv.naturality f

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a :
  Eq.{v_1 + 1} (α :=
    Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0))
          X) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
    (Quiver.Hom.unop
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Quiver.Hom.op
          (Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0)) X)
    (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X))))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
        Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
        Opposite.unop X)
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0))
          X) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
    (Quiver.Hom.unop
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Quiver.Hom.op
          (Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)))))

Tactic:
dsimp [opShiftFunctorEquivalence]

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a :
  Eq.{v_1 + 1} (α :=
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X) ⟶
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0))
          X))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
    (Quiver.Hom.unop
      (Quiver.Hom.op
          (Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X)
    (Quiver.Hom.op
        (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X) ⟶
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0))
          X))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
    (Quiver.Hom.unop
      (Quiver.Hom.op
          (Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))))

Tactic:
dsimp [opShiftFunctorEquivalence]

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
m n p : ℤ
h : autoParam (m + n = p) opShiftFunctorEquivalence_add_unitIso_hom_app_eq._auto_1
⊢ n + m = p

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

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ Eq.{v_1 + 1} (α :=
    X ⟶
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X))))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))
      (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))))
        (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))))
        (Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))) ≫
          Quiver.Hom.op
            (Functor.map (shiftFunctor C p)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X))))))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))
      (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))))
        (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
        (Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) ≫
          Quiver.Hom.op
            (Functor.map (shiftFunctor C p)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X))))))

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

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n : ℤ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
        (Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
            X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)))
    (Functor.map (shiftFunctor C n)
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)))
    (Quiver.Hom.unop
      (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)))))

Tactic:
Quiver.Hom.op_inj ((opShiftFunctorEquivalence C n).unit_app_inverse X).symm

Premises used: Quiver.Hom.op_inj, CategoryTheory.Equivalence.unit_app_inverse, Eq.symm, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n : ℤ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
        (Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
            X)))
    (Functor.map (shiftFunctor C n)
      (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)))
    (Quiver.Hom.unop
      (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)))))

Tactic:
Quiver.Hom.op_inj ((opShiftFunctorEquivalence C n).unitInv_app_inverse X).symm

Premises used: Quiver.Hom.op_inj, CategoryTheory.Equivalence.unitInv_app_inverse, Eq.symm, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n : ℤ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n)))
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (Functor.map (shiftFunctor Cᵒᵖ n) (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X))

Tactic:
(opShiftFunctorEquivalence C n).counitInv_app_functor X

Premises used: CategoryTheory.Functor.op, CategoryTheory.shiftFunctor, Int.add.match_1, CategoryTheory.Equivalence.counitInv_app_functor, Int.add, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, Int.neg