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' 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)

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₁)
⊢ T₁.hom.op.toLoc ≫ (Over.Hom.left f).op.toLoc = T₂.hom.op.toLoc

Tactic:
F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app _ _ _ _ _ _ _ _ (by
          simp only [← Quiver.Hom.comp_toLoc, ← op_comp, Over.w_assoc])

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.map (Over.Hom.left f).op.toLoc).toFunctor.map
              ((F.mapComp' q.op.toLoc ?m.259 (q.op.toLoc ≫ T₁.hom.op.toLoc) ?m.264).hom.toNatTrans.app N) ≫
            (F.mapComp' ?m.259 (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ?m.265).inv.toNatTrans.app
              ((F.map q.op.toLoc).toFunctor.obj 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₁)
⊢ { as := op S' } ⟶ { as := op T₁.left }

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₁)
⊢ q.op.toLoc ≫ ?m.259 = q.op.toLoc ≫ T₁.hom.op.toLoc

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₁)
⊢ ?m.259 ≫ (Over.Hom.left f).op.toLoc = T₂.hom.op.toLoc

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