-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ ⋙
          shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (a₁ + a₂)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂ (a₁ + a₂) ⋯)) X)
    (Functor.map (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₁ ((φ : (a : A) → B) a₁) ⋯)) X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₂ : B))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₁ : B)) X))
        (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₂ ((φ : (a : A) → B) a₂) ⋯))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₁ : B)) X))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor C (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B))) X)
          (NatTrans.app
            (Iso.inv
              (shiftFunctorAdd' C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂)
                (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) ⋯))
            X)
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso C φ (a₁ + a₂)
                (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
            X)))
have simp : NatTrans.app (Iso.inv (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂ (a₁ + a₂) sorry)) X =
  CategoryStruct.comp (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₂ : B))
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X))
    (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₂ ((φ : (a : A) → B) a₂) sorry))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₂ : B))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₂ : B))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₁ : B)) X))
        (Functor.map (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₂ : B))
          (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₁ ((φ : (a : A) → B) a₁) sorry)) X))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor C (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B))) X)
          (NatTrans.app
            (Iso.inv
              (shiftFunctorAdd' C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂)
                (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) sorry))
            X)
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso C φ (a₁ + a₂)
                (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
            X)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₂ : B))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (a₁ + a₂)) X)
Tactic: simp only [Functor.comp_obj, NatTrans.naturality_assoc]