-- 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₃ : 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
G : Functor.{v_1, v_2, u_1, u_4} C D
inst_7 : G.CommShift B
τ : F ⟶ G
inst_8 : CommShift τ B
x : A
x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
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 (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1))
      (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x)
        (obj (PullbackShift.functor φ G) x_1)))
    (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 : B)) x_1))
      (F.map (app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) 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_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_1))
      (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 : B)) (F.obj x_1))
          (app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_1)
          (app (Iso.inv (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_1) ≫
            map (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (τ.app 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_1) ⟶
          obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x)
            (obj (PullbackShift.functor φ G) x_1)))
    (τ.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1) ≫
      CategoryStruct.comp (Y :=
        G.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_1))
        (G.map (app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_1) :
          G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1) ⟶
            G.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_1))
        (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 : B)) (G.obj x_1))
            (app (Iso.hom (commShiftIso G ((φ : (a : A) → B) x))) x_1)
            (app (Iso.inv (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (G.obj x_1)) :
          G.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_1) ⟶
            obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x)
              (obj (PullbackShift.functor φ G) x_1)))
⊢ 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 (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1))
      (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x)
        (obj (PullbackShift.functor φ G) x_1)))
    (app (Iso.hom (commShiftIso (PullbackShift.functor φ F) x)) x_1 ≫
      map (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (τ.app x_1))
    (τ.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1) ≫
      app (Iso.hom (commShiftIso (PullbackShift.functor φ G) x)) x_1)

Tactic:
simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, comp_app, comp_obj, whiskerRight_app, whiskerLeft_app,
      assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.commShiftPullback_iso_eq, CategoryTheory.Functor.isoWhiskerRight_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.isoWhiskerLeft_hom, rfl