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