-- 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₁)
⊢ 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))
have 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
                              sorry)).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
                              sorry)).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
                              sorry)).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
                              sorry)).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: ext g