-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
dsimp :
  CategoryStruct.comp (Y :=
      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.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
        Opposite.unop (Opposite.op X) ⟶
          Opposite.unop
            (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) (Opposite.op X))))))
      (Functor.map (shiftFunctor C n) (Quiver.Hom.unop x + Quiver.Hom.unop y) :
        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))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) =
    HAdd.hAdd (α := ShiftedHom X Y n)
      (CategoryStruct.comp (Y :=
        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.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
          Opposite.unop (Opposite.op X) ⟶
            Opposite.unop
              (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) (Opposite.op X))))))
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop 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} (shiftFunctor Cᵒᵖ n) (Opposite.op X))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))
      (CategoryStruct.comp (Y :=
        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.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
          Opposite.unop (Opposite.op X) ⟶
            Opposite.unop
              (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) (Opposite.op X))))))
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop y) :
          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))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))
⊢ (Equiv.symm (opEquiv n) : (a : ShiftedHom (Opposite.op Y) (Opposite.op X) n) → ShiftedHom X Y n) (x + y) =
    HAdd.hAdd (α := ShiftedHom X Y n) (β := ShiftedHom X Y n)
      ((Equiv.symm (opEquiv n) : (a : ShiftedHom (Opposite.op Y) (Opposite.op X) n) → ShiftedHom X Y n) x :
        ShiftedHom X Y n)
      ((Equiv.symm (opEquiv n) : (a : ShiftedHom (Opposite.op Y) (Opposite.op X) n) → ShiftedHom X Y n) y :
        ShiftedHom X Y n)

Tactic:
dsimp [opEquiv_symm_apply]

Premises used: CategoryTheory.ShiftedHom.opEquiv_symm_apply