-- 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₁)
h :
  ∀ (g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)),
    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)
⊢ Eq (α :=
    ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁) ⟶
      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₂))
    (((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₂)))
    (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))

Tactic:
ext g