-- 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 (α :=
    Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
      (obj (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1) ⋙ PullbackShift.functor φ F) x_2)
      (obj (PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1)) x_2))
    (NatTrans.app
      (Iso.hom
        (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B) ⋙ F)
          (isoWhiskerRight (pullbackShiftIso C φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) ⋯) F :
            shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (x + x_1) ⋙ F ≅
              shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B) ⋙ F)
          (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) (x + x_1) : B))
              (commShiftIso F ((φ : (a : A) → B) (x + x_1)))
              (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) ⋯))) :
            shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) (x + x_1) : B) ⋙ F ≅
              PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (x + x_1))))
      x_2)
    (NatTrans.app
      (Iso.hom
        (CommShift.isoAdd
          (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B) ⋙ F)
            (isoWhiskerRight (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯) F :
              shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ F ≅
                shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B) ⋙ F)
            (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B))
                (commShiftIso F ((φ : (a : A) → B) x))
                (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯))) :
              shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B) ⋙ F ≅
                PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x))
          (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F)
            (isoWhiskerRight (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯) F :
              shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1 ⋙ F ≅
                shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F)
            (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
                (commShiftIso F ((φ : (a : A) → B) x_1))
                (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ x_1 ((φ : (a : A) → B) x_1) ⋯))) :
              shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B) ⋙ F ≅
                PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1))))
      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 :=
        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.hom (commShiftIso F ((φ : (a : A) → B) (x + x_1)))) x_2)
        (NatTrans.app (Iso.inv (pullbackShiftIso D φ (x + x_1) ((φ : (a : A) → B) (x + x_1)) sorry)) (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)))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x x_1)) 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 (PullbackShift.{v_1, u_1, u_2, u_3} C φ) 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 (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) 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_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)))
      (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))
            (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_2)))
          (NatTrans.app (Iso.hom (commShiftIso F ((φ : (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))
          (NatTrans.app (Iso.inv (pullbackShiftIso D φ x_1 ((φ : (a : A) → B) x_1) sorry))
              (F.obj (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 :=
              obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                (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)))
              (map (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                  (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) sorry)) x_2)) :
                obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                    (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_2)) ⟶
                  obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                    (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 :=
                  obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                    (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 (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                    (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_2))
                  (map (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                      (NatTrans.app (Iso.inv (pullbackShiftIso D φ x ((φ : (a : A) → B) x) sorry)) (F.obj x_2)) ≫
                    NatTrans.app (Iso.inv (shiftFunctorAdd (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 (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x_1)
                    (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_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)) ⟶
          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: simp only [PullbackShift.functor, comp_obj, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, NatTrans.comp_app, whiskerRight_app, whiskerLeft_app,
      CommShift.isoAdd_hom_app, map_comp, assoc]