Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ (shiftFunctorOpIso C (-n) n ⋯).hom.app (Opposite.op X) ≫
      ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctorOpIso C n (-n) ⋯).inv.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
          (shiftFunctorOpIso C (-n) n ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj (Opposite.op ((shiftFunctor C n).obj X))) =
    ((shiftFunctorCompIsoId C n (-n) ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ (-n)).obj (Opposite.op X)))).op ≫
      ((shiftFunctor C (-n)).map
            ((shiftFunctor C n).map ((shiftFunctorOpIso C (-n) n hmn).hom.app (Opposite.op X)).unop)).op ≫
        ((shiftFunctor C (-n)).map
              ((shiftFunctorOpIso C (-n) n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
          ((shiftFunctor C (-n)).map
                ((shiftFunctorOpIso C (-n) n ⋯).hom.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
            ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C n).obj X)).op ≫
              ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)).op ≫
                ((shiftFunctor C n).map
                      ((shiftFunctorOpIso C n (-n) ⋯).inv.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
                  (shiftFunctorOpIso C (-n) n ⋯).inv.app
                    ((shiftFunctor Cᵒᵖ n).obj (Opposite.op ((shiftFunctor C n).obj X)))

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ ((shiftFunctorOpIso C (-n) n ⋯).hom.app (Opposite.op X) ≫
        ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)).op ≫
          ((shiftFunctor C n).map
                ((shiftFunctorOpIso C n (-n) ⋯).inv.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
            (shiftFunctorOpIso C (-n) n ⋯).inv.app
              ((shiftFunctor Cᵒᵖ n).obj (Opposite.op ((shiftFunctor C n).obj X)))).unop =
    (((shiftFunctorCompIsoId C n (-n) ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ (-n)).obj (Opposite.op X)))).op ≫
        ((shiftFunctor C (-n)).map
              ((shiftFunctor C n).map ((shiftFunctorOpIso C (-n) n hmn).hom.app (Opposite.op X)).unop)).op ≫
          ((shiftFunctor C (-n)).map
                ((shiftFunctorOpIso C (-n) n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
            ((shiftFunctor C (-n)).map
                  ((shiftFunctorOpIso C (-n) n ⋯).hom.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
              ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C n).obj X)).op ≫
                ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)).op ≫
                  ((shiftFunctor C n).map
                        ((shiftFunctorOpIso C n (-n) ⋯).inv.app (Opposite.op ((shiftFunctor C n).obj X))).unop).op ≫
                    (shiftFunctorOpIso C (-n) n ⋯).inv.app
                      ((shiftFunctor Cᵒᵖ n).obj (Opposite.op ((shiftFunctor C n).obj X)))).unop