-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
this :
  Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op Z' : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map a'.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₁.obj (α j))))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map a'.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₂.obj (α j)))))
    (CategoryStruct.comp (Y :=
        Functor.obj (C := (↑(F.obj { as := op Z : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map r.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map a.op.toLoc))
            (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
              (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₁.obj (α j)))))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯)))
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₁.obj (α j))))
        (Functor.map (Cat.Hom.toFunctor (F.map r.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map a.op.toLoc)) (φ.hom j)) ≫
          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯)))
            (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
              (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₂.obj (α j)))) :
      Quiver.Hom (V := (↑(F.obj { as := op Z' : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map a'.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₁.obj (α j))))
        (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map a'.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₂.obj (α j)))))
    (Functor.map (Cat.Hom.toFunctor (F.map a'.op.toLoc)) (φ.hom j) :
      Quiver.Hom (V := (↑(F.obj { as := op Z' : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map a'.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₁.obj (α j))))
        (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map a'.op.toLoc))
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D₂.obj (α j)))))
⊢ ((F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i) ≫
        Functor.map (Cat.Hom.toFunctor (F.map r.op.toLoc)) (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯) ≫
          (F.mapComp' (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc a.op.toLoc)
                    r.op.toLoc
                    (CategoryStruct.comp (Y := { as := op Z : LocallyDiscrete Cᵒᵖ })
                      (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc a.op.toLoc)
                      r.op.toLoc)
                    ⋯).inv.toNatTrans.app
            (D₁.obj (α j))) ≫
      ((F.mapComp' (p' j).op.toLoc a'.op.toLoc
                    (CategoryStruct.comp (Y := { as := op Z : LocallyDiscrete Cᵒᵖ })
                      (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc a.op.toLoc)
                      r.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D₁.obj (α j)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map a'.op.toLoc)) (φ.hom j) ≫
            (F.mapComp' (p' j).op.toLoc a'.op.toLoc
                      (CategoryStruct.comp (Y := { as := op Z : LocallyDiscrete Cᵒᵖ })
                        (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc
                          a.op.toLoc)
                        r.op.toLoc)
                      ⋯).inv.toNatTrans.app
              (D₂.obj (α j))) ≫
        (F.mapComp' (CategoryStruct.comp (Y := { as := op (X' j) }) (p' j).op.toLoc a.op.toLoc) r.op.toLoc
                    (CategoryStruct.comp (Y := { as := op Z })
                      (CategoryStruct.comp (Y := { as := op (X' j) }) (p' j).op.toLoc a.op.toLoc) r.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D₂.obj (α j)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map r.op.toLoc)) (D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯) ≫
            (F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i) =
    NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯))) (D₁.obj i) ≫
      Functor.map (Cat.Hom.toFunctor (F.map r.op.toLoc))
          (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
            ((F.mapComp' (p' j).op.toLoc a.op.toLoc
                          (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc
                            a.op.toLoc)
                          ⋯).hom.toNatTrans.app
                  (D₁.obj (α j)) ≫
                Functor.map (Cat.Hom.toFunctor (F.map a.op.toLoc)) (φ.hom j) ≫
                  (F.mapComp' (p' j).op.toLoc a.op.toLoc
                            (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc
                              a.op.toLoc)
                            ⋯).inv.toNatTrans.app
                    (D₂.obj (α j))) ≫
              D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯) ≫
        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯))) (D₂.obj i)

Tactic:
simp only [Category.assoc, Functor.map_comp, ← this,
    Cat.Hom.inv_hom_id_toNatTrans_app_assoc,
    mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc F
    (p' j).op.toLoc a.op.toLoc r.op.toLoc ((p' j).op.toLoc ≫ a.op.toLoc) a'.op.toLoc
      (((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc) rfl (by grind) (by grind),
    ← mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc F
    (p' j).op.toLoc a.op.toLoc r.op.toLoc ((p' j).op.toLoc ≫ a.op.toLoc) a'.op.toLoc
      (((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc) rfl (by grind) (by grind)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, Quiver.Hom.op, CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.CategoryStruct.comp, Quiver.Hom.toLoc, CategoryTheory.Functor.map_comp, rfl