-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
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
⊢ (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)
have 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))
Tactic: dsimp [opEquiv_symm_apply]