-- 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 : 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 (PullbackShift.functor φ F)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) x))
      (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
        (obj (PullbackShift.functor φ F) x)))
    (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) 0 : B)) x))
      (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) ⋯)) x) :
        F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0)
              x) ⟶
          F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x))
      (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) 0 : B)) (F.obj x))
          (NatTrans.app (Iso.hom (commShiftIso F ((φ : (a : A) → B) 0))) x)
          (NatTrans.app (Iso.inv (pullbackShiftIso D φ 0 ((φ : (a : A) → B) 0) ⋯)) (F.obj x)) :
        F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x) ⟶
          obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
            (obj (PullbackShift.functor φ F) x)))
    (NatTrans.app (Iso.hom (CommShift.isoZero (PullbackShift.functor φ F) A)) x)
have w : Eq (α :=
  Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
    (obj (PullbackShift.functor φ F)
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) x))
    (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
      (obj (PullbackShift.functor φ F) x)))
  (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) 0 : B)) x))
    (F.map (NatTrans.app (Iso.hom (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) sorry)) x) :
      F.obj
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0)
            x) ⟶
        F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x))
    (F.map
          (NatTrans.app (Iso.hom (shiftFunctorZero' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) ((φ : (a : A) → B) 0) sorry))
            x) ≫
        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) 0 : B)) (F.obj x))
          (NatTrans.app (Iso.inv (shiftFunctorZero' (PullbackShift.{v_2, u_4, u_2, u_3} D φ) ((φ : (a : A) → B) 0) sorry))
              (F.obj x) :
            obj.{v_2, v_2, u_4, u_4} (𝟭 (PullbackShift.{v_2, u_4, u_2, u_3} D φ)) (F.obj x) ⟶
              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) 0 : B))
                (F.obj x))
          (NatTrans.app (Iso.inv (pullbackShiftIso D φ 0 ((φ : (a : A) → B) 0) sorry)) (F.obj x) :
            obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) 0 : B)) (F.obj x) ⟶
              obj.{v_2, v_2, u_4, u_4}
                (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x) ⟶
        obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
          (obj (PullbackShift.functor φ F) x)))
  (CategoryStruct.comp (Y :=
    obj (PullbackShift.functor φ F)
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x))
    (map (PullbackShift.functor φ F) (NatTrans.app (Iso.hom (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) sorry)) x) :
      Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
        (obj (PullbackShift.functor φ F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0)
            x))
        (obj (PullbackShift.functor φ F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x)))
    (map (PullbackShift.functor φ F) (NatTrans.app (Iso.hom (shiftFunctorZero' C ((φ : (a : A) → B) 0) sorry)) x) ≫
        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) 0 : B))
            (obj (PullbackShift.functor φ F) x))
          (NatTrans.app (Iso.inv (shiftFunctorZero' D ((φ : (a : A) → B) 0) sorry)) (obj (PullbackShift.functor φ F) x) :
            obj.{v_2, v_2, u_4, u_4} (𝟭 D) (obj (PullbackShift.functor φ F) x) ⟶
              obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) 0 : B))
                (obj (PullbackShift.functor φ F) x))
          (NatTrans.app (Iso.inv (pullbackShiftIso D φ 0 ((φ : (a : A) → B) 0) sorry)) (obj (PullbackShift.functor φ F) x) :
            obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) 0 : B))
                (obj (PullbackShift.functor φ F) x) ⟶
              obj.{v_2, v_2, u_4, u_4}
                (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
                (obj (PullbackShift.functor φ F) x)) :
      Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
        (obj (PullbackShift.functor φ F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) x))
        (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
          (obj (PullbackShift.functor φ F) x))))
Tactic: simp only [F.commShiftIso_zero' (A := B) (φ 0) (by rw [map_zero]), CommShift.isoZero'_hom_app,
      assoc, CommShift.isoZero_hom_app, pullbackShiftFunctorZero'_hom_app, map_comp,
      pullbackShiftFunctorZero'_inv_app]