-- 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_1 : Functor.{v_1, v_2, u_1, u_4} C D
inst_7 : G_1.CommShift B
E : Type u_5
inst_8 : Category.{v_3, u_5} E
inst_9 : HasShift.{v_3, u_5, u_3} E B
G : Functor.{v_2, v_3, u_4, u_5} D E
inst_10 : G.CommShift B
x : A
x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
w :
  Eq (α :=
    Quiver.Hom (V := PullbackShift.{v_3, u_5, u_2, u_3} E φ)
      (obj (PullbackShift.functor φ (F ⋙ G))
        (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x)
        (obj (C := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ G)
          (obj (PullbackShift.functor φ F) x_1))))
    (app (Iso.hom (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x)) x_1 ≫
        map (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (𝟙 (obj (PullbackShift.functor φ (F ⋙ G)) x_1)) :
      Quiver.Hom (V := PullbackShift.{v_3, u_5, u_2, u_3} E φ)
        (obj (PullbackShift.functor φ (F ⋙ G))
          (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x)
          (obj (C := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ G)
            (obj (PullbackShift.functor φ F) x_1))))
    (𝟙
          (obj (PullbackShift.functor φ (F ⋙ G))
            (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
              (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F)
                (PullbackShift.functor φ G))
              x))
          x_1 :
      Quiver.Hom (V := PullbackShift.{v_3, u_5, u_2, u_3} E φ)
        (obj (PullbackShift.functor φ (F ⋙ G))
          (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x)
          (obj (C := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ G)
            (obj (PullbackShift.functor φ F) x_1))))
⊢ Eq (α :=
    Quiver.Hom (V := PullbackShift.{v_3, u_5, u_2, u_3} E φ)
      (obj (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ PullbackShift.functor φ (F ⋙ G)) x_1)
      (obj
        (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F) (PullbackShift.functor φ G) ⋙
          shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x)
        x_1))
    (app
      (Iso.hom (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x) ≫
        whiskerRight (Iso.hom (PullbackShift.natIsoComp φ F G))
          (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x))
      x_1)
    (app
      (whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x)
          (Iso.hom (PullbackShift.natIsoComp φ F G)) ≫
        Iso.hom
          (commShiftIso
            (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F) (PullbackShift.functor φ G))
            x))
      x_1)

Tactic:
dsimp [PullbackShift.natIsoComp]

Premises used: CategoryTheory.NatTrans.PullbackShift.natIsoComp