-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F G : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
inst_6 : G.CommShift A
τ : F ⟶ G
inst_7 : CommShift τ A
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
w :
  Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x)
        (Functor.obj (OppositeShift.functor A G) x_1))
      (Functor.obj (OppositeShift.functor A F)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)))
    (Functor.map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) (app (OppositeShift.natTrans A τ) x_1) ≫
      app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)
    (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1 ≫
      app (OppositeShift.natTrans A τ)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x)
        (Functor.obj (OppositeShift.functor A G) x_1))
      (Functor.obj (OppositeShift.functor A F)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)))
    (CategoryStruct.comp (Y :=
      Functor.obj (OppositeShift.functor A G)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
      (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x)
          (Functor.obj (OppositeShift.functor A F) x_1))
        (app (Iso.hom (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1 ≫
          Functor.map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) (app (OppositeShift.natTrans A τ) x_1))
        (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)))
    (CategoryStruct.comp (Y :=
      Functor.obj (OppositeShift.functor A G)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
      (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x)
          (Functor.obj (OppositeShift.functor A F) x_1))
        (app (OppositeShift.natTrans A τ)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1) ≫
          app (Iso.hom (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)
        (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)))

Tactic:
simp only [assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app, Functor.comp_obj,
      comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_app_assoc