-- Module: Mathlib.CategoryTheory.Shift.Pullback
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₂)
simp :
  NatTrans.app (Iso.inv (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂ (a₁ + 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 (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X))
      (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₂ ((φ : (a : A) → B) 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 (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₁) ⋯)) 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)) :
        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)
⊢ 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)))

Tactic:
simp only [Functor.comp_obj, NatTrans.naturality_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.NatTrans.naturality_assoc