-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
rw :
  Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X' i₁) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α i₁)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' i₁).op.toLoc))
          (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₁)))))) M)))
      (Functor.obj (C := (↑(F.obj { as := op (X' i₂) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op S' : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (f' i₂).op.toLoc)) (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M))))
    (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (Iso.symm
                    (F.mapComp' p.op.toLoc (f' i₁).op.toLoc
                      (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) p.op.toLoc (f' i₁).op.toLoc)
                      ⋯) ≪≫
                  F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₁)))) (p' i₁).op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₁).op.toLoc) ⋯)))
            M) ≫
        (F.mapComp' (f' i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app
            (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M) ≫
          (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
            (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M) :
      Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Functor.obj (C := (↑(F.obj { as := op (X' i₁) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X (α i₁)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' i₁).op.toLoc))
            (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₁)))))) M)))
        (Functor.obj (C := (↑(F.obj { as := op (X' i₂) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op S' : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (f' i₂).op.toLoc)) (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M))))
    (pullFunctorObjHom w (ofObj M) (f₁ ≫ f' i₁) f₁ f₂ ⋯ ⋯ ≫
        Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
          (NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (Iso.symm
                    (F.mapComp' p.op.toLoc (f' i₂).op.toLoc
                      (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) p.op.toLoc (f' i₂).op.toLoc)
                      ⋯) ≪≫
                  F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₂)))) (p' i₂).op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₂).op.toLoc) ⋯)))
            M) :
      Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Functor.obj (C := (↑(F.obj { as := op (X' i₁) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X (α i₁)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' i₁).op.toLoc))
            (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₁)))))) M)))
        (Functor.obj (C := (↑(F.obj { as := op (X' i₂) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op S' : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (f' i₂).op.toLoc)) (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M))))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) ((F.isoMapOfCommSq ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (f' i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app
          (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M) ≫
        (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
          (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M) =
    pullFunctorObjHom w (ofObj M) (f₁ ≫ f' i₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) ((F.isoMapOfCommSq ⋯).inv.toNatTrans.app M)

Tactic:
rw [F.isoMapOfCommSq_eq _ _ rfl, F.isoMapOfCommSq_eq _ _ rfl]

Premises used: CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq, rfl