-- 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.{v_2 + 1} (α := (shiftFunctor C (a + b) ⋙ F).obj x ⟶ (F ⋙ shiftFunctor D (a + b)).obj x)
    (NatTrans.app
      (Iso.hom
        (NatIso.removeOp
          (Iso.symm
            (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a)
              (commShiftIso (OppositeShift.functor A F) b)))))
      x)
    (NatTrans.app
      (Iso.hom
        (CommShift.isoAdd (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) a)))
          (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) b)))))
      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) (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))
Tactic: simp only [comp_obj, NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app, op_obj,
      CommShift.isoAdd_inv_app, unop_comp, Category.assoc,
      CommShift.isoAdd_hom_app]