-- 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 S' : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map q.op.toLoc)) (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M)))
    (CategoryStruct.comp (Y :=
        Functor.obj (C := (↑(F.obj { as := op (X' i₁) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (Functor.obj
            (Cat.Hom.toFunctor
              (F.map (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) p.op.toLoc (f' i₁).op.toLoc)))
            M))
        (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (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))
        (CategoryStruct.comp (Y :=
          Functor.obj
            (Cat.Hom.toFunctor
              (F.map (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) p.op.toLoc q.op.toLoc)))
            M)
          (NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (F.mapComp' (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₁).op.toLoc) f₁.op.toLoc
                  (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc q.op.toLoc) ⋯)))
            M)
          (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.hom
                  (F.mapComp' p.op.toLoc q.op.toLoc (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc q.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))) ≫
      (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))
    (CategoryStruct.comp (Y :=
        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)))
        ((F.mapComp' (p' i₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' i₁).op.toLoc ⋯).inv.toNatTrans.app
            (obj (f := f) (ofObj M) (α i₁)) ≫
          hom (ofObj M) (q ≫ p) (f₁ ≫ p' i₁) (f₂ ≫ p' i₂) ⋯ ⋯ ≫
            (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' i₂).op.toLoc ⋯).hom.toNatTrans.app
              (obj (f := f) (ofObj M) (α i₂)))
        (Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.inv
                  (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) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.hom
                  (F.mapComp' p.op.toLoc (f' i₂).op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) 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))
⊢ 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))))
    (CategoryStruct.comp (Y :=
        Functor.obj (C := (↑(F.obj { as := op (X' i₁) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (Functor.obj
            (Cat.Hom.toFunctor
              (F.map (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) p.op.toLoc (f' i₁).op.toLoc)))
            M))
        (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
          (NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (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))
        (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
            (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.hom
                  (F.mapComp' p.op.toLoc (f' i₁).op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) 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
                  (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) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.hom
                  (F.mapComp' p.op.toLoc (f' i₂).op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) 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))))

Tactic:
rw [← F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc p.op.toLoc
            (f' i₁).op.toLoc f₁.op.toLoc _ q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) rfl
            (by grind) (by grind) M,
          pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' i₁) (f₂ ≫ p' i₂),
          ← cancel_mono ((F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc
            (by grind)).inv.toNatTrans.app _)]

Premises used: Quiver.Hom.op, CategoryTheory.cancel_mono, CategoryTheory.CategoryStruct.comp, Quiver.Hom.toLoc, CategoryTheory.Pseudofunctor.mapComp', CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, rfl