-- 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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
h :
  Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ })))
          (D.obj (α j))) ≫
      (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X (α j))))) (p' j).op.toLoc (p' j).op.toLoc ⋯).inv.toNatTrans.app
          (D.obj (α j)) ≫
        D.hom (p' j ≫ f (α j)) (p' j) (p' j ≫ q' (α j) ≫ p' (β (α j))) ⋯ ⋯ ≫
          (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j) ≫ p' (β (α j))))) (p' j).op.toLoc
                      (p' j ≫ q' (α j) ≫ p' (β (α j))).op.toLoc ⋯).hom.toNatTrans.app
              (D.obj (α (β (α j)))) ≫
            CategoryStruct.comp (Y :=
              Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
                (Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                  (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))))
                  (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))))
                    (D.obj (α (β (α j)))))))
              (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
                (NatTrans.app
                  (Cat.Hom₂.toNatTrans
                    (Iso.hom
                      (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))
                        (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))
                        (CategoryStruct.comp (Y := { as := op (X' (β (α j))) })
                          (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))
                          (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))))
                        ⋯)))
                  (D.obj (α (β (α j))))))
              (CategoryStruct.comp (Y :=
                Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                  (Cat.Hom.toFunctor
                    (F.map
                      (CategoryStruct.comp (Y := { as := op (X (α j)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))
                        (p' j).op.toLoc)))
                  (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))))
                    (D.obj (α (β (α j))))))
                (NatTrans.app
                    (Cat.Hom₂.toNatTrans
                      (Iso.inv
                        (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))) (p' j).op.toLoc
                          (CategoryStruct.comp (Y := { as := op (X (α j)) })
                            (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))) (p' j).op.toLoc)
                          ⋯)))
                    (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                      (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))))
                      (D.obj (α (β (α j))))) :
                  Quiver.Hom (V := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                      (Functor.comp (D := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                        (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))))
                        (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)))
                      (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                        (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))))
                        (D.obj (α (β (α j))))))
                    (Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                      (Cat.Hom.toFunctor
                        (F.map
                          (CategoryStruct.comp (Y := { as := op (X (α j)) })
                            (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))) (p' j).op.toLoc)))
                      (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                        (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))))
                        (D.obj (α (β (α j)))))))
                ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))) (p' j ≫ q' (α j)).op.toLoc
                              (p' j ≫ q' (α j) ≫ p' (β (α j))).op.toLoc ⋯).inv.toNatTrans.app
                      (D.obj (α (β (α j)))) ≫
                    D.hom (p' j ≫ f (α j)) (p' j ≫ q' (α j) ≫ p' (β (α j))) (p' j) ⋯ ⋯ ≫
                      (F.mapComp' (p' j).op.toLoc (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X' j)))) (p' j).op.toLoc
                                  ⋯).hom.toNatTrans.app
                          (D.obj (α j)) ≫
                        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X' j) })))
                          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))) :
                  Quiver.Hom (V := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                      (Cat.Hom.toFunctor (F.map (p' j ≫ q' (α j)).op.toLoc))
                      (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                        (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))))
                        (D.obj (α (β (α j))))))
                    (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                      (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))))) =
    𝟙
      (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j)))
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j)))
      (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))))
    (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ })))
          (D.obj (α j))) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
          (D.hom (f (α j)) (𝟙 (X (α j))) (q' (α j) ≫ p' (β (α j))) ⋯ ⋯) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
            (Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
              (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))))
              (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))))) (D.obj (α (β (α j)))))))
          (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
            (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.hom
                  (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))
                    (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))
                    (CategoryStruct.comp (Y := { as := op (X' (β (α j))) })
                      (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))) (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))))
                    ⋯)))
              (D.obj (α (β (α j))))))
          (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.inv
                  (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))) (p' j).op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X (α j)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))
                      (p' j).op.toLoc)
                    ⋯)))
              (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))))) (D.obj (α (β (α j))))) ≫
            pullFunctorObjHom w D (p' j ≫ q' (α j) ≫ f' (β (α j))) (p' j ≫ q' (α j)) (𝟙 (X' j)) ⋯ ⋯ ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X' j) : LocallyDiscrete Cᵒᵖ })))
                (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                  (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j)))))
    (𝟙
      (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))))

Tactic:
rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ (p' _ ≫ f _) (p' _ ≫ q' _ ≫ p' _) (p' _) (by simp)
        (by simp [w', reassoc_of% w]),
      map_eq_pullHom_assoc _ (p' j) (p' j) (p' _ ≫ q' _ ≫ p' _) (by simp) (by simp),
      D.pullHom_hom _ _ (p' j ≫ f _) (by simp) _ _ (by simp)
        (by simp [w, reassoc_of% w']) _ _ (by simp) rfl]

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, rfl