Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (F.map (p' j).op.toLoc).toFunctor.map ((F.mapId { as := op (X (α j)) }).inv.toNatTrans.app (D.obj (α j))) ≫
      (F.mapComp' (𝟙 { as := op (X (α j)) }) (p' j).op.toLoc (p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
        D.hom (p' j ≫ f (α j)) (p' j) (p' j ≫ q' (α j) ≫ p' (β (α j))) ⋯ ⋯ ≫
          (F.mapComp' ((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) (p' j).op.toLoc
                      (((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) ≫ (p' j).op.toLoc) ⋯).hom.toNatTrans.app
              (D.obj (α (β (α j)))) ≫
            (F.map (p' j).op.toLoc).toFunctor.map
                ((F.mapComp' (p' (β (α j))).op.toLoc (q' (α j)).op.toLoc ((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc)
                          ⋯).hom.toNatTrans.app
                  (D.obj (α (β (α j))))) ≫
              (F.mapComp' (q' (α j)).op.toLoc (p' j).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc)
                          ⋯).inv.toNatTrans.app
                  ((F.map (p' (β (α j))).op.toLoc).toFunctor.obj (D.obj (α (β (α j))))) ≫
                (F.mapComp' (p' (β (α j))).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc)
                            (((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) ≫ (p' j).op.toLoc) ⋯).inv.toNatTrans.app
                    (D.obj (α (β (α j)))) ≫
                  D.hom (p' j ≫ f (α j)) (p' j ≫ q' (α j) ≫ p' (β (α j))) (p' j) ⋯ ⋯ ≫
                    (F.mapComp' (p' j).op.toLoc (𝟙 { as := op (X' j) }) (p' j).op.toLoc ⋯).hom.toNatTrans.app
                        (D.obj (α j)) ≫
                      (F.mapId { as := op (X' j) }).hom.toNatTrans.app
                        ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))) =
    𝟙 ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j)))

Tactic:
rw [← F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc _ _ _ _ _ _ rfl rfl (by simp),
      mapComp'_comp_id_hom_app, mapComp'_id_comp_inv_app_assoc, ← Functor.map_comp_assoc,
      Cat.Hom.inv_hom_id_toNatTrans_app]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (F.map (p' j).op.toLoc).toFunctor.map (𝟙 ((𝟙 (F.obj { as := op (X (α j)) })).toFunctor.obj (D.obj (α j)))) ≫
      D.hom (p' j ≫ f (α j)) (p' j) (p' j ≫ q' (α j) ≫ p' (β (α j))) ⋯ ⋯ ≫
        (F.mapComp' (p' (β (α j))).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc)
                    (((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) ≫ (p' j).op.toLoc) ⋯).hom.toNatTrans.app
            (D.obj (α (β (α j)))) ≫
          (F.mapComp' (q' (α j)).op.toLoc (p' j).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc) ⋯).hom.toNatTrans.app
              ((F.map (p' (β (α j))).op.toLoc).toFunctor.obj (D.obj (α (β (α j))))) ≫
            (F.mapComp' (q' (α j)).op.toLoc (p' j).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc)
                        ⋯).inv.toNatTrans.app
                ((F.map (p' (β (α j))).op.toLoc).toFunctor.obj (D.obj (α (β (α j))))) ≫
              (F.mapComp' (p' (β (α j))).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc)
                          (((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) ≫ (p' j).op.toLoc) ⋯).inv.toNatTrans.app
                  (D.obj (α (β (α j)))) ≫
                D.hom (p' j ≫ f (α j)) (p' j ≫ q' (α j) ≫ p' (β (α j))) (p' j) ⋯ ⋯ ≫
                  (F.mapId { as := op (X' j) }).inv.toNatTrans.app
                      ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))) ≫
                    (F.mapId { as := op (X' j) }).hom.toNatTrans.app
                      ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))) =
    𝟙 ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j)))