-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
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
h :
  ∀ (j : ι'),
    ((pullFunctor F w).map
              ((Iso.symm (pullFunctorIdIso F S) ≪≫
                      Iso.trans (Y := pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) ⋯)
                        (pullFunctorIso F ⋯ ⋯ :
                          Iso (C := F.DescentData f ⥤ F.DescentData f) (pullFunctor F ⋯)
                            (pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) ⋯))
                        (Iso.symm (pullFunctorCompIso F w w' (𝟙 S) ⋯ ⋯) :
                          pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) ⋯ ≅
                            pullFunctor F w ⋙ pullFunctor F w')).hom.app
                D) ≫
            (Iso.trans (Y := pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) ⋯)
                    (pullFunctorCompIso F w' w (𝟙 S') ⋯ ⋯ :
                      pullFunctor F w' ⋙ pullFunctor F w ≅
                        pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) ⋯)
                    (pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S' :
                      Iso (C := F.DescentData f' ⥤ F.DescentData f')
                        (pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) ⋯)
                        (𝟭 (F.DescentData f')))).hom.app
              ((pullFunctor F w).obj D)).hom
        j =
      Hom.hom (𝟙 ((pullFunctor F w).obj D)) j
⊢ (pullFunctor F w).map
        ((Iso.symm (pullFunctorIdIso F S) ≪≫
                Iso.trans (Y := pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) ⋯)
                  (pullFunctorIso F ⋯ ⋯ :
                    Iso (C := F.DescentData f ⥤ F.DescentData f) (pullFunctor F ⋯)
                      (pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) ⋯))
                  (Iso.symm (pullFunctorCompIso F w w' (𝟙 S) ⋯ ⋯) :
                    pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) ⋯ ≅
                      pullFunctor F w ⋙ pullFunctor F w')).hom.app
          D) ≫
      (Iso.trans (Y := pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) ⋯)
              (pullFunctorCompIso F w' w (𝟙 S') ⋯ ⋯ :
                pullFunctor F w' ⋙ pullFunctor F w ≅
                  pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) ⋯)
              (pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S' :
                Iso (C := F.DescentData f' ⥤ F.DescentData f')
                  (pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) ⋯)
                  (𝟭 (F.DescentData f')))).hom.app
        ((pullFunctor F w).obj D) =
    𝟙 ((pullFunctor F w).obj D)

Tactic:
ext j