-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
a :
  Eq (α :=
    op
        (F.obj
          (unop
            (obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C n))
              X))) ⟶
      op (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))))
    (Quiver.Hom.op
      (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X))))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (obj.{v_2, v_2, u_2, u_2}
            (Equivalence.inverse (opShiftFunctorEquivalence D n) ⋙ Equivalence.functor (opShiftFunctorEquivalence D n))
            (op (F.obj (unop X)))))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))
        (CategoryStruct.comp (Y :=
          unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((shiftFunctor C n ⋙ F).obj (unop X)))))
          (Quiver.Hom.unop
              (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F n)) (unop X)))) :
            unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((F ⋙ shiftFunctor D n).obj (unop X)))) ⟶
              unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((shiftFunctor C n ⋙ F).obj (unop X)))))
          (Quiver.Hom.unop
              (NatTrans.app (Iso.hom (commShiftIso F.op n))
                (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) :
            unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) ⟶
              unop ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))))
⊢ Eq (α :=
    F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)) ⟶
      F.obj
        (unop
          (obj.{v_1, v_1, u_1, u_1}
            (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
            X)))
    (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)))
    (CategoryStruct.comp (Y :=
      unop
        (obj.{v_2, v_2, u_2, u_2}
          (Equivalence.inverse (opShiftFunctorEquivalence D n) ⋙ Equivalence.functor (opShiftFunctorEquivalence D n))
          (op (F.obj (unop X)))))
      (Quiver.Hom.unop
        (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))
      (CategoryStruct.comp (Y :=
        unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((shiftFunctor C n ⋙ F).obj (unop X)))))
        (Quiver.Hom.unop
            (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F n)) (unop X)))) :
          unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((F ⋙ shiftFunctor D n).obj (unop X)))) ⟶
            unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((shiftFunctor C n ⋙ F).obj (unop X)))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.hom (commShiftIso F.op n)) (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) :
          unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) ⟶
            unop ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))))))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj