-- 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 Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ Eq.{v_1 + 1} (α := ShiftedHom X Z c)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
        Opposite.unop (Opposite.op X) ⟶
          Opposite.unop
            (Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
      (Functor.map (shiftFunctor C b)
            (CategoryStruct.comp (Y :=
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))))
                (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a)))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) :
                  Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)) ⟶
                    Opposite.unop
                      (Opposite.op
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                          (Opposite.unop
                            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a)
                              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))))))
                (Functor.map (shiftFunctor C a) (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ a) g)) :
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                      (Opposite.unop
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a)
                          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))) ⟶
                    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y)))) ≫
              Functor.map (shiftFunctor C a) (Quiver.Hom.unop f)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c ⋯)) Z :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
        Opposite.unop (Opposite.op X) ⟶
          Opposite.unop
            (Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
      (Functor.map (shiftFunctor C b)
            (CategoryStruct.comp (Y :=
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
              (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y) ≫ g) :
                Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)) ⟶
                  Opposite.unop
                    (Opposite.op
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
              (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))) ⟶
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Z)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c ⋯)) Z :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
have erw : Eq.{v_1 + 1} (α := ShiftedHom X Z c)
  (CategoryStruct.comp (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
      Opposite.unop (Opposite.op X) ⟶
        Opposite.unop
          (Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
    (Functor.map (shiftFunctor C b)
          (CategoryStruct.comp (Y :=
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                (Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))))
              (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a)))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) :
                Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)) ⟶
                  Opposite.unop
                    (Opposite.op
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                        (Opposite.unop
                          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a)
                            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))))))
              (Functor.map (shiftFunctor C a) (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ a) g)) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                    (Opposite.unop
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a)
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))) ⟶
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y)))) ≫
            Functor.map (shiftFunctor C a) (Quiver.Hom.unop f)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c sorry)) Z :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
  (CategoryStruct.comp (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
      Opposite.unop (Opposite.op X) ⟶
        Opposite.unop
          (Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
    (Functor.map (shiftFunctor C b)
          (CategoryStruct.comp (Y :=
            Opposite.unop
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
            (Quiver.Hom.unop
                (Functor.map (shiftFunctor Cᵒᵖ a ⋙ Functor.op (shiftFunctor C a)) g ≫
                  NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a)))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) :
              Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)) ⟶
                Opposite.unop
                  (Opposite.op
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
            (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f) :
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))) ⟶
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Z)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c sorry)) Z :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
Tactic: erw [← NatTrans.naturality]