-- 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) ≫
        Functor.map (Cat.Hom.toFunctor (F.map (Over.Hom.left f).op.toLoc)) g ≫
          Functor.map (Cat.Hom.toFunctor (F.map (Over.Hom.left f).op.toLoc))
              (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)
⊢ (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)

Tactic:
simp only [Category.assoc, Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp