-- 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₁)
⊢ (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)
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) ≫
      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) 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: simp only [Category.assoc, Functor.map_comp]