-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
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
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
have h : Eq (α :=
  Quiver.Hom (V := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
    (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 (p' j).op.toLoc)) (D.obj (α j))))
  (CategoryStruct.comp (Y :=
    Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
      (Functor.obj (C := (↑(F.obj { as := op (X' (β (α j))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))))
        (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))))) (D.obj (α (β (α j)))))))
    (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc))
      (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ })))
          (D.obj (α j)) ≫
        D.hom (𝟙 (X (α j)) ≫ f (α j)) (𝟙 (X (α j))) (q' (α j) ≫ p' (β (α j))) sorry sorry ≫
          NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.hom
                (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))
                  (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))
                  (CategoryStruct.comp (Y := { as := op (X' (β (α j))) })
                    (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))) (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))))
                  sorry)))
            (D.obj (α (β (α j))))))
    (NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.inv
            (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))) (p' j).op.toLoc
              (CategoryStruct.comp (Y := { as := op (X (α j)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j))))
                (p' j).op.toLoc)
              sorry)))
        (Functor.obj (C := (↑(F.obj { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j))))))) (D.obj (α (β (α j))))) ≫
      pullFunctorObjHom w D ((p' j ≫ q' (α j)) ≫ f' (β (α j))) (p' j ≫ q' (α j)) (𝟙 (X' j)) sorry sorry ≫
        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X' j) : LocallyDiscrete Cᵒᵖ })))
          (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 (p' j).op.toLoc)) (D.obj (α j))))
Tactic: dsimp