-- 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 : ℤ
hmn : -n + n = 0
a :
  Eq.{v_1 + 1} (α :=
    Opposite.unop
        (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.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))
    (Quiver.Hom.unop
      (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯)) (Opposite.op 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))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
          (Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
          (Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯))
                    (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
            NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯))
              (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) X))))))
    (Quiver.Hom.unop
      (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 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X))))))
        (Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯))
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))))
        (Quiver.Hom.op
            (Functor.map (shiftFunctor C (-n))
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n hmn)) (Opposite.op X))))) ≫
          Quiver.Hom.op
              (Functor.map (shiftFunctor C (-n))
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n hmn))
                    (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
            Quiver.Hom.op
                (Functor.map (shiftFunctor C (-n))
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯))
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
              Quiver.Hom.op
                  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
                CategoryStruct.comp (Y :=
                  Opposite.op
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n) ⋙ shiftFunctor C n)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
                  (Quiver.Hom.op
                    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
                  (Quiver.Hom.op
                      (Functor.map (shiftFunctor C n)
                        (Quiver.Hom.unop
                          (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯))
                            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
                    NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯))
                      (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) X)))))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X) ⟶
      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.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯)) (Opposite.op 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))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
        (Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
        (Quiver.Hom.op
            (Functor.map (shiftFunctor C n)
              (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯))
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯))
            (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) 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 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X))))))
      (Quiver.Hom.op
        (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯))
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))))
      (Quiver.Hom.op
          (Functor.map (shiftFunctor C (-n))
            (Functor.map (shiftFunctor C n)
              (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n hmn)) (Opposite.op X))))) ≫
        Quiver.Hom.op
            (Functor.map (shiftFunctor C (-n))
              (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n hmn))
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
          Quiver.Hom.op
              (Functor.map (shiftFunctor C (-n))
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n ⋯))
                    (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
            Quiver.Hom.op
                (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
              CategoryStruct.comp (Y :=
                Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n) ⋙ shiftFunctor C n)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
                (Quiver.Hom.op
                  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
                (Quiver.Hom.op
                    (Functor.map (shiftFunctor C n)
                      (Quiver.Hom.unop
                        (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯))
                          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
                  NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n ⋯))
                    (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) X))))))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj