-- 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
b₃ : B
h₃ : b₃ = (φ : (a : A) → B) (a₁ + a₂)
obtain :
  ∀
    (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)))
⊢ 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 b₃) X)
          (NatTrans.app (Iso.inv (shiftFunctorAdd' C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂) b₃ ⋯)) X)
          (NatTrans.app (Iso.inv (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃)) X)))

Tactic:
obtain rfl : b₃ = φ a₁ + φ a₂ := by rw [h₃, φ.map_add]

Premises used: DFunLike.coe, rfl