-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
x x_1 : A
x_2 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1)) x_2) ⟶
      obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2))
    (CategoryStruct.comp (Y :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
      (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) ⋯)) x_2) :
        F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1)) x_2) ⟶
          F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
      (CategoryStruct.comp (Y :=
          F.obj
            (obj.{v_1, v_1, u_1, u_1}
              (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                ((φ : (a : A) → B) x_1 : B))
              (obj.{v_1, v_1, u_1, u_1}
                (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                  ((φ : (a : A) → B) x : B))
                x_2)))
          (F.map
              (NatTrans.app
                (Iso.hom
                  (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) ((φ : (a : A) → B) x)
                    ((φ : (a : A) → B) x_1) ((φ : (a : A) → B) (x + x_1)) ⋯))
                x_2) :
            F.obj
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) (x + x_1) : B))
                  x_2) ⟶
              F.obj
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) x_1 : B))
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_2)))
          (CategoryStruct.comp (Y :=
              obj.{v_2, v_2, u_4, u_4}
                (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                  ((φ : (a : A) → B) x_1 : B))
                (F.obj
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_2)))
              (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x_1)))
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_2) :
                (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                          ((φ : (a : A) → B) x_1 : B) ⋙
                        F).obj
                    (obj.{v_1, v_1, u_1, u_1}
                      (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                        ((φ : (a : A) → B) x : B))
                      x_2) ⟶
                  (F ⋙
                        shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                          ((φ : (a : A) → B) x_1 : B)).obj
                    (obj.{v_1, v_1, u_1, u_1}
                      (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                        ((φ : (a : A) → B) x : B))
                      x_2))
              (CategoryStruct.comp (Y :=
                  obj.{v_2, v_2, u_4, u_4}
                    (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                      ((φ : (a : A) → B) x_1 : B))
                    (obj.{v_2, v_2, u_4, u_4}
                      (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                        ((φ : (a : A) → B) x : B))
                      (F.obj x_2)))
                  (map
                      (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                        ((φ : (a : A) → B) x_1 : B))
                      (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_2) :
                    obj.{v_2, v_2, u_4, u_4}
                        (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                          ((φ : (a : A) → B) x_1 : B))
                        (F.obj
                          (obj.{v_1, v_1, u_1, u_1}
                            (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                              ((φ : (a : A) → B) x : B))
                            x_2)) ⟶
                      obj.{v_2, v_2, u_4, u_4}
                        (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                          ((φ : (a : A) → B) x_1 : B))
                        (obj.{v_2, v_2, u_4, u_4}
                          (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                            ((φ : (a : A) → B) x : B))
                          (F.obj x_2)))
                  (CategoryStruct.comp (Y :=
                      obj.{v_2, v_2, u_4, u_4}
                        (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B)) (F.obj x_2))
                      (NatTrans.app
                        (Iso.inv
                          (shiftFunctorAdd' (PullbackShift.{v_2, u_4, u_2, u_3} D φ) ((φ : (a : A) → B) x)
                            ((φ : (a : A) → B) x_1) ((φ : (a : A) → B) (x + x_1)) ⋯))
                        (F.obj x_2))
                      (NatTrans.app (Iso.inv (pullbackShiftIso D φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) ⋯))
                        (F.obj x_2)) :
                    obj.{v_2, v_2, u_4, u_4}
                        (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                          ((φ : (a : A) → B) x_1 : B))
                        (obj.{v_2, v_2, u_4, u_4}
                          (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                            ((φ : (a : A) → B) x : B))
                          (F.obj x_2)) ⟶
                      obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                        (F.obj x_2)) :
                obj.{v_2, v_2, u_4, u_4}
                    (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                      ((φ : (a : A) → B) x_1 : B))
                    (F.obj
                      (obj.{v_1, v_1, u_1, u_1}
                        (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                          ((φ : (a : A) → B) x : B))
                        x_2)) ⟶
                  obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                    (F.obj x_2)) :
            F.obj
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) x_1 : B))
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_2)) ⟶
              obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2)) :
        F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2) ⟶
          obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2)))
    (CategoryStruct.comp (Y :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
      (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) ⋯)) x_2) :
        F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1)) x_2) ⟶
          F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
      (CategoryStruct.comp (Y :=
          F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
          (F.map
            (NatTrans.app
              (Iso.hom
                (shiftFunctorAdd' C ((φ : (a : A) → B) x) ((φ : (a : A) → B) x_1) ((φ : (a : A) → B) (x + x_1)) ⋯))
              x_2))
          (CategoryStruct.comp (Y :=
            F.obj
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
            (F.map
              (NatTrans.app (Iso.inv (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
            (F.map
                (map (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
                  (NatTrans.app (Iso.inv (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_2)) ≫
              F.map
                  (NatTrans.app (Iso.hom (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯))
                    (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_2)) ≫
                CategoryStruct.comp (Y :=
                  (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F).obj
                    (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2))
                  ((shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F).map
                    (NatTrans.app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_2))
                  (CategoryStruct.comp (Y :=
                    (F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B)).obj
                      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                        x_2))
                    (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x_1)))
                        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                          x_2) :
                      (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F).obj
                          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                            x_2) ⟶
                        (F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B)).obj
                          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                            x_2))
                    (CategoryStruct.comp (Y :=
                        obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                          (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B))
                            (F.obj x_2)))
                        (map (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                            (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_2) :
                          obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                              (F.obj
                                (obj.{v_1, v_1, u_1, u_1}
                                  (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)) ⟶
                            obj.{v_2, v_2, u_4, u_4}
                              (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                              (obj.{v_2, v_2, u_4, u_4}
                                (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B)) (F.obj x_2)))
                        (CategoryStruct.comp (Y :=
                            obj.{v_2, v_2, u_4, u_4}
                              (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B)) (F.obj x_2))
                            (NatTrans.app
                              (Iso.inv
                                (shiftFunctorAdd' D ((φ : (a : A) → B) x) ((φ : (a : A) → B) x_1)
                                  ((φ : (a : A) → B) (x + x_1)) ⋯))
                              (F.obj x_2))
                            (NatTrans.app (Iso.inv (pullbackShiftIso D φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) ⋯))
                              (F.obj x_2)) :
                          obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                              (obj.{v_2, v_2, u_4, u_4}
                                (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B)) (F.obj x_2)) ⟶
                            obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                              (F.obj x_2)) :
                      obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                          (F.obj
                            (obj.{v_1, v_1, u_1, u_1}
                              (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)) ⟶
                        obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                          (F.obj x_2))))) :
        F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2) ⟶
          obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2)))
have w : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1)) x_2) ⟶
    obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2))
  (CategoryStruct.comp (Y :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
    (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) sorry)) x_2) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1)) x_2) ⟶
        F.obj
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
    (CategoryStruct.comp (Y :=
        F.obj
          (obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B) ((φ : (a : A) → B) x_1 : B))
            (obj.{v_1, v_1, u_1, u_1}
              (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B) ((φ : (a : A) → B) x : B))
              x_2)))
        (F.map
            (NatTrans.app
              (Iso.hom
                (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) ((φ : (a : A) → B) x) ((φ : (a : A) → B) x_1)
                  ((φ : (a : A) → B) (x + x_1)) sorry))
              x_2) :
          F.obj
              (obj.{v_1, v_1, u_1, u_1}
                (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                  ((φ : (a : A) → B) (x + x_1) : B))
                x_2) ⟶
            F.obj
              (obj.{v_1, v_1, u_1, u_1}
                (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                  ((φ : (a : A) → B) x_1 : B))
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) x : B))
                  x_2)))
        (CategoryStruct.comp (Y :=
            obj.{v_2, v_2, u_4, u_4}
              (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                ((φ : (a : A) → B) x_1 : B))
              (F.obj
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) x : B))
                  x_2)))
            (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x_1)))
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) x : B))
                  x_2) :
              (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                        ((φ : (a : A) → B) x_1 : B) ⋙
                      F).obj
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_2) ⟶
                (F ⋙
                      shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                        ((φ : (a : A) → B) x_1 : B)).obj
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_2))
            (CategoryStruct.comp (Y :=
                obj.{v_2, v_2, u_4, u_4}
                  (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                    ((φ : (a : A) → B) x_1 : B))
                  (obj.{v_2, v_2, u_4, u_4}
                    (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    (F.obj x_2)))
                (map
                    (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                      ((φ : (a : A) → B) x_1 : B))
                    (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_2) :
                  obj.{v_2, v_2, u_4, u_4}
                      (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                        ((φ : (a : A) → B) x_1 : B))
                      (F.obj
                        (obj.{v_1, v_1, u_1, u_1}
                          (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                            ((φ : (a : A) → B) x : B))
                          x_2)) ⟶
                    obj.{v_2, v_2, u_4, u_4}
                      (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                        ((φ : (a : A) → B) x_1 : B))
                      (obj.{v_2, v_2, u_4, u_4}
                        (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                          ((φ : (a : A) → B) x : B))
                        (F.obj x_2)))
                (CategoryStruct.comp (Y :=
                    obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B))
                      (F.obj x_2))
                    (NatTrans.app
                      (Iso.inv
                        (shiftFunctorAdd' (PullbackShift.{v_2, u_4, u_2, u_3} D φ) ((φ : (a : A) → B) x)
                          ((φ : (a : A) → B) x_1) ((φ : (a : A) → B) (x + x_1)) sorry))
                      (F.obj x_2))
                    (NatTrans.app (Iso.inv (pullbackShiftIso D φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) sorry))
                      (F.obj x_2)) :
                  obj.{v_2, v_2, u_4, u_4}
                      (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                        ((φ : (a : A) → B) x_1 : B))
                      (obj.{v_2, v_2, u_4, u_4}
                        (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                          ((φ : (a : A) → B) x : B))
                        (F.obj x_2)) ⟶
                    obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                      (F.obj x_2)) :
              obj.{v_2, v_2, u_4, u_4}
                  (shiftFunctor.{v_2, u_4, u_3} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := B)
                    ((φ : (a : A) → B) x_1 : B))
                  (F.obj
                    (obj.{v_1, v_1, u_1, u_1}
                      (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                        ((φ : (a : A) → B) x : B))
                      x_2)) ⟶
                obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                  (F.obj x_2)) :
          F.obj
              (obj.{v_1, v_1, u_1, u_1}
                (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                  ((φ : (a : A) → B) x_1 : B))
                (obj.{v_1, v_1, u_1, u_1}
                  (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                    ((φ : (a : A) → B) x : B))
                  x_2)) ⟶
            obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2) ⟶
        obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2)))
  (CategoryStruct.comp (Y :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
    (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) sorry)) x_2) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1)) x_2) ⟶
        F.obj
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2))
    (CategoryStruct.comp (Y :=
        F.obj
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
        (F.map
          (NatTrans.app
            (Iso.hom (shiftFunctorAdd' C ((φ : (a : A) → B) x) ((φ : (a : A) → B) x_1) ((φ : (a : A) → B) (x + x_1)) sorry))
            x_2))
        (CategoryStruct.comp (Y :=
          F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
          (F.map
            (NatTrans.app (Iso.inv (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) sorry))
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
          (CategoryStruct.comp (Y :=
            obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B))
              (F.obj x_2))
            (CategoryStruct.comp (Y :=
                obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                  (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B))
                    (F.obj x_2)))
                (CategoryStruct.comp (Y :=
                    (F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B)).obj
                      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                        x_2))
                    (CategoryStruct.comp (Y :=
                      (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F).obj
                        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                          x_2))
                      (CategoryStruct.comp (Y :=
                        F.obj
                          (obj.{v_1, v_1, u_1, u_1}
                            (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
                            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_2)))
                        (F.map
                            (NatTrans.app (Iso.hom (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) sorry))
                              (obj.{v_1, v_1, u_1, u_1}
                                (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)) ≫
                          F.map
                            (map (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
                              (NatTrans.app (Iso.inv (pullbackShiftIso C φ x ((φ : (a : A) → B) x) sorry)) x_2)))
                        ((shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F).map
                          (NatTrans.app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) sorry)) x_2)))
                      (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x_1)))
                        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                          x_2)))
                    (map (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                      (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_2)) :
                  F.obj
                      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
                        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                          x_2)) ⟶
                    obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                      (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B))
                        (F.obj x_2)))
                (NatTrans.app
                    (Iso.inv
                      (shiftFunctorAdd' D ((φ : (a : A) → B) x) ((φ : (a : A) → B) x_1) ((φ : (a : A) → B) (x + x_1))
                        sorry))
                    (F.obj x_2) :
                  obj.{v_2, v_2, u_4, u_4}
                      (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B) ⋙
                        shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                      (F.obj x_2) ⟶
                    obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B))
                      (F.obj x_2)) :
              F.obj
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
                    (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B))
                      x_2)) ⟶
                obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B))
                  (F.obj x_2))
            (NatTrans.app (Iso.inv (pullbackShiftIso D φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) sorry)) (F.obj x_2) :
              obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B))
                  (F.obj x_2) ⟶
                obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))
                  (F.obj x_2)))) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B)) x_2) ⟶
        obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) (F.obj x_2)))
Tactic: slice_rhs 4 5 => rw [← map_comp, (pullbackShiftIso C φ _ _ rfl).hom.naturality, map_comp]