-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsPrestack (goal)
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₁)
⊢ 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)
have 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) sorry)))
        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)
                  sorry).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)
                    sorry).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) sorry)))
      N =
  (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc sorry).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) sorry)))
              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) sorry)))
            N) ≫
      (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc sorry).inv.toNatTrans.app
        (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) N)
Tactic: dsimp [pullHom]