-- 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 a : ℤ
x y :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
rw :
  HAdd.hAdd (α := ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n) (β :=
        ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n)
        ((Equiv.symm (opEquiv n) :
              (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
                ShiftedHom X ((shiftFunctor C a).obj Y) n)
            x :
          ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n)
        ((Equiv.symm (opEquiv n) :
              (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
                ShiftedHom X ((shiftFunctor C a).obj Y) n)
            y :
          ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y =
    HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            x ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            y ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
⊢ (Equiv.symm (opEquiv n) :
          (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
            X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
        (x + y) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y =
    HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            x ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            y ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
have rw₁ : HAdd.hAdd (α := X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y) (β :=
    X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
    ((Equiv.symm (opEquiv n) :
            (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
              ShiftedHom X ((shiftFunctor C a).obj Y) n)
          x ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
    ((Equiv.symm (opEquiv n) :
            (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
              ShiftedHom X ((shiftFunctor C a).obj Y) n)
          y ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y) =
  HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
    ((Equiv.symm (opEquiv n) :
            (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
              X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
          x ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
    ((Equiv.symm (opEquiv n) :
            (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
              X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
          y ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
Tactic: rw [opEquiv_symm_add, Preadditive.add_comp]