-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this_1 :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
Y : C
j : ι'
p : Z.left ⟶ X' j
ψ : D₁ ⟶ D₂
hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i
this_2 : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom
this :
  Functor.map (Cat.Hom.toFunctor (F.map Z.hom.op.toLoc)) (ψ.hom i) ≫ D₂.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      Functor.map
        (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op (X' j) }) (p' j).op.toLoc p.op.toLoc)))
        (ψ.hom (α j))
⊢ (F.mapComp' (𝟙 { as := op (X i) : LocallyDiscrete Cᵒᵖ }) Z.hom.op.toLoc Z.hom.op.toLoc ⋯).hom.toNatTrans.app
        (D₁.obj i) ≫
      Functor.map (Cat.Hom.toFunctor (F.map Z.hom.op.toLoc))
          (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i) : LocallyDiscrete Cᵒᵖ }))) (D₁.obj i) ≫
            ψ.hom i ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op (X i) : LocallyDiscrete Cᵒᵖ })))
                (D₂.obj i)) ≫
        (F.mapComp' (𝟙 { as := op (X i) : LocallyDiscrete Cᵒᵖ }) Z.hom.op.toLoc Z.hom.op.toLoc ⋯).inv.toNatTrans.app
          (D₂.obj i) =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      ((F.mapComp' (p' j).op.toLoc p.op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) (p' j).op.toLoc p.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D₁.obj (α j)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
              (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (ψ.hom (α j))) ≫
            (F.mapComp' (p' j).op.toLoc p.op.toLoc
                      (CategoryStruct.comp (Y := { as := op (X' j) }) (p' j).op.toLoc p.op.toLoc) ⋯).inv.toNatTrans.app
              (D₂.obj (α j))) ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯

Tactic:
simp [mapComp'_inv_naturality, Cat.Hom.comp_toFunctor,
        Functor.comp_obj, Cat.Hom.hom_inv_id_toNatTrans_app_assoc, ← reassoc_of% this,
        D₂.hom_self _ _ rfl, F.mapComp'_id_comp_inv_app, ← Functor.map_comp,
        F.mapComp'_id_comp_hom_app_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.Pseudofunctor.DescentData.hom_self, CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc, rfl