-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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 : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
a b : A
x : Cᵒᵖ
⊢ Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
              (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x)))))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x))))
          (Quiver.Hom.op (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj (Opposite.unop x)))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F)
          (NatTrans.app (Iso.hom (shiftFunctorAdd (OppositeShift.{v_1, u_1, u_3} C A) a b)) x) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
            (obj (OppositeShift.functor A F)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x)))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b))
              (Opposite.unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x))))
          (map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
              (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd (OppositeShift.{v_2, u_2, u_3} D A) a b))
              (obj (OppositeShift.functor A F) x)) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b)) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b))
          (obj (OppositeShift.functor A F) x)))
have w : Eq (α :=
  Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
    Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
  (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
      CategoryStruct.comp (Y :=
        Opposite.op
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
            (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x)))))
        (Quiver.Hom.op
          (NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x))))
        (Quiver.Hom.op (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
          Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj (Opposite.unop x)))) :
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
  (map (OppositeShift.functor A F) (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
      CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
          (obj (OppositeShift.functor A F)
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x)))
        (Quiver.Hom.op
          (NatTrans.app (Iso.inv (commShiftIso F b))
            (Opposite.unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x))))
        (map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
            (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
          Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (Opposite.unop (obj (OppositeShift.functor A F) x)))) :
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (obj (OppositeShift.functor A F)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b)) x))
      (obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b))
        (obj (OppositeShift.functor A F) x)))
Tactic: erw [oppositeShiftFunctorAdd_inv_app, oppositeShiftFunctorAdd_hom_app]