-- 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 (α :=
    G.obj (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)) ⟶
      obj.{v_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1)))
    (CategoryStruct.comp (Y :=
      G.obj (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)))
      (G.map (F.map (app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_1)) :
        G.obj (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)) ⟶
          G.obj
            (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 :=
          G.obj
            (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)))
          (G.map (app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_1) :
            G.obj
                (F.obj
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_1)) ⟶
              G.obj
                (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)))
          (CategoryStruct.comp (Y :=
              obj.{v_3, v_3, u_5, u_5} (shiftFunctor.{v_3, u_5, u_3} E (A := B) ((φ : (a : A) → B) x : B))
                (G.obj (F.obj x_1)))
              (app (Iso.hom (commShiftIso G ((φ : (a : A) → B) x))) (F.obj x_1))
              (app (Iso.inv (pullbackShiftIso E φ x ((φ : (a : A) → B) x) ⋯)) (G.obj (F.obj x_1))) :
            G.obj
                (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)) ⟶
              obj.{v_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1))) :
        G.obj
            (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1))))
    (CategoryStruct.comp (Y :=
      G.obj (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)))
      (G.map (F.map (app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_1)) :
        G.obj (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)) ⟶
          G.obj
            (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)))
      (G.map (app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_1) ≫
          CategoryStruct.comp (Y :=
            obj.{v_3, v_3, u_5, u_5} (shiftFunctor.{v_3, u_5, u_3} E (A := B) ((φ : (a : A) → B) x : B))
              (G.obj (F.obj x_1)))
            (G.map
                (𝟙
                  (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 G ((φ : (a : A) → B) x))) (F.obj x_1))
            (app (Iso.inv (pullbackShiftIso E φ x ((φ : (a : A) → B) x) ⋯)) (G.obj (F.obj x_1))) :
        G.obj
            (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1))))
⊢ Eq (α :=
    G.obj (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)) ⟶
      obj.{v_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1)))
    (CategoryStruct.comp (Y :=
      G.obj (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)))
      (G.map (F.map (app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_1)) :
        G.obj (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)) ⟶
          G.obj
            (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 :=
          G.obj
            (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)))
          (G.map (app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_1) :
            G.obj
                (F.obj
                  (obj.{v_1, v_1, u_1, u_1}
                    (shiftFunctor.{v_1, u_1, u_3} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := B)
                      ((φ : (a : A) → B) x : B))
                    x_1)) ⟶
              G.obj
                (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)))
          (CategoryStruct.comp (Y :=
              obj.{v_3, v_3, u_5, u_5} (shiftFunctor.{v_3, u_5, u_3} E (A := B) ((φ : (a : A) → B) x : B))
                (G.obj (F.obj x_1)))
              (app (Iso.hom (commShiftIso G ((φ : (a : A) → B) x))) (F.obj x_1))
              (app (Iso.inv (pullbackShiftIso E φ x ((φ : (a : A) → B) x) ⋯)) (G.obj (F.obj x_1))) :
            G.obj
                (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)) ⟶
              obj.{v_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1))) :
        G.obj
            (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1))))
    (CategoryStruct.comp (Y :=
      G.obj (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)))
      (G.map (F.map (app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_1)) :
        G.obj (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)) ⟶
          G.obj
            (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 :=
          G.obj
            (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)))
          (G.map (app (Iso.hom (commShiftIso F ((φ : (a : A) → B) x))) x_1))
          (CategoryStruct.comp (Y :=
            G.obj (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (F.obj x_1)))
            (G.map (app (Iso.inv (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_1)))
            (CategoryStruct.comp (Y :=
              G.obj
                (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)))
              (G.map (app (Iso.hom (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_1)) :
                G.obj (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (F.obj x_1)) ⟶
                  G.obj
                    (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)))
              (CategoryStruct.comp (Y :=
                  obj.{v_3, v_3, u_5, u_5} (shiftFunctor.{v_3, u_5, u_3} E (A := B) ((φ : (a : A) → B) x : B))
                    (G.obj (F.obj x_1)))
                  (app (Iso.hom (commShiftIso G ((φ : (a : A) → B) x))) (F.obj x_1))
                  (app (Iso.inv (pullbackShiftIso E φ x ((φ : (a : A) → B) x) ⋯)) (G.obj (F.obj x_1))) :
                G.obj
                    (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)) ⟶
                  obj.{v_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x)
                    (G.obj (F.obj x_1))))) :
        G.obj
            (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_3, v_3, u_5, u_5} (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x) (G.obj (F.obj x_1))))

Tactic:
slice_rhs 3 4 => rw [← G.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app