-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
simp :
  (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
              ((F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
            (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (obj' i₂)
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
            Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂) ≫
              (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
        (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (obj' i₂)

Tactic:
simp only [Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp