-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  CategoryStruct.comp (Y :=
      Functor.obj (C := (↑(F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)))
        (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (obj i₁)))
      (NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.hom
            (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)
              gf₁.op.toLoc ⋯)))
        (obj i₁))
      (NatTrans.app
          (Cat.Hom₂.toNatTrans
            (Iso.hom
              (F.mapComp' p.op.toLoc g.op.toLoc
                (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) ⋯)))
          (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (obj i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂)) ≫
          NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.inv
                  (F.mapComp' p.op.toLoc g.op.toLoc
                    (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) ⋯)))
              (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (obj' i₂)) ≫
            NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.inv
                  (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)
                    gf₂.op.toLoc ⋯)))
              (obj' i₂)) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc
                (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (obj' i₂)
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
              ((F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
            (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (obj' i₂)

Tactic:
rw [F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
    _ _ _ _ _ _ (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst])
    rfl (by cat_disch),
    F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app _ _ _ _ _ _
      (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]) rfl (by cat_disch)]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, rfl, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc