Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).inv.toNatTrans.app M ≫
      (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                  ⋯).hom.toNatTrans.app
          M ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                      ⋯).inv.toNatTrans.app
              N ≫
            (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).hom.toNatTrans.app N =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
              ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).hom.toNatTrans.app N) ≫
            (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
              ((F.map q.op.toLoc).toFunctor.obj N)

Tactic:
F.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc _ _ _ _ _ _ rfl _ rfl,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ?m.244).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                      ⋯).inv.toNatTrans.app
              N ≫
            (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).hom.toNatTrans.app N =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
              ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).hom.toNatTrans.app N) ≫
            (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
              ((F.map q.op.toLoc).toFunctor.obj N)

C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ T₁.hom.op.toLoc ≫ (Over.Hom.left f).op.toLoc = T₂.hom.op.toLoc