-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
S' : C
q : S' ⟶ S
T₁ T₂ : Over.{v, u} S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
h :
  (NatTrans.app
          (Cat.Hom₂.toNatTrans
            (Iso.inv
              (F.mapComp' q.op.toLoc T₂.hom.op.toLoc
                (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₂.hom.op.toLoc) ⋯)))
          M ≫
        (F.mapComp' (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₁.hom.op.toLoc)
                    (Over.Hom.left f).op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₂.hom.op.toLoc)
                    ⋯).hom.toNatTrans.app
            M ≫
          Functor.map (Cat.Hom.toFunctor (F.map (Over.Hom.left f).op.toLoc)) g ≫
            (F.mapComp' (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₁.hom.op.toLoc)
                      (Over.Hom.left f).op.toLoc
                      (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₂.hom.op.toLoc)
                      ⋯).inv.toNatTrans.app
              N) ≫
      NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.hom
            (F.mapComp' q.op.toLoc T₂.hom.op.toLoc
              (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₂.hom.op.toLoc) ⋯)))
        N =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) M) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (Over.Hom.left f).op.toLoc))
          ((NatTrans.app
                (Cat.Hom₂.toNatTrans
                  (Iso.inv
                    (F.mapComp' q.op.toLoc T₁.hom.op.toLoc
                      (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₁.hom.op.toLoc) ⋯)))
                M ≫
              g) ≫
            NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.hom
                  (F.mapComp' q.op.toLoc T₁.hom.op.toLoc
                    (CategoryStruct.comp (Y := { as := op S' : LocallyDiscrete Cᵒᵖ }) q.op.toLoc T₁.hom.op.toLoc) ⋯)))
              N) ≫
        (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
          (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) N)
⊢ Eq (α :=
    Functor.obj
      (F.presheafHom (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) M)
        (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) N))
      (op T₂))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((Over.map q).op ⋙ F.presheafHom M N).map (op f) ≫
          Iso.hom
            ((fun (T : (Over.{v, u} S')ᵒᵖ) ↦
                (Equiv.trans
                    ((Cat.Hom.toNatIso
                            (F.mapComp' q.op.toLoc (unop T).hom.op.toLoc ((Over.map q).obj (unop T)).hom.op.toLoc
                              ⋯)).app
                        M).homFromEquiv
                    ((Cat.Hom.toNatIso
                            (F.mapComp' q.op.toLoc (unop T).hom.op.toLoc ((Over.map q).obj (unop T)).hom.op.toLoc
                              ⋯)).app
                        N).homToEquiv).toIso)
              (op T₂))))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (T : (Over.{v, u} S')ᵒᵖ) ↦
                (Equiv.trans
                    ((Cat.Hom.toNatIso
                            (F.mapComp' q.op.toLoc (unop T).hom.op.toLoc ((Over.map q).obj (unop T)).hom.op.toLoc
                              ⋯)).app
                        M).homFromEquiv
                    ((Cat.Hom.toNatIso
                            (F.mapComp' q.op.toLoc (unop T).hom.op.toLoc ((Over.map q).obj (unop T)).hom.op.toLoc
                              ⋯)).app
                        N).homToEquiv).toIso)
              (op T₁)) ≫
          Functor.map
            (F.presheafHom (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) M)
              (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) N))
            (op f)))
      g)

Tactic:
dsimp [pullHom]

Premises used: CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom