-- 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
⊢ (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)
have 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)) sorry)
                      (pullFunctorIso F sorry sorry :
                        Iso (C := F.DescentData f ⥤ F.DescentData f) (pullFunctor F sorry)
                          (pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) sorry))
                      (Iso.symm (pullFunctorCompIso F w w' (𝟙 S) sorry sorry) :
                        pullFunctor F (p := 𝟙 S) (α := α ∘ β) (p' := fun (x : ι) ↦ q' x ≫ p' (β x)) sorry ≅
                          pullFunctor F w ⋙ pullFunctor F w')).hom.app
              D) ≫
          (Iso.trans (Y := pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) sorry)
                  (pullFunctorCompIso F w' w (𝟙 S') sorry sorry :
                    pullFunctor F w' ⋙ pullFunctor F w ≅
                      pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) sorry)
                  (pullFunctorIso F sorry sorry ≪≫ pullFunctorIdIso F S' :
                    Iso (C := F.DescentData f' ⥤ F.DescentData f')
                      (pullFunctor F (p := 𝟙 S') (α := β ∘ α) (p' := fun (x : ι') ↦ p' x ≫ q' (α x)) sorry)
                      (𝟭 (F.DescentData f')))).hom.app
            ((pullFunctor F w).obj D)).hom
      j =
    Hom.hom (𝟙 ((pullFunctor F w).obj D)) j
Tactic: ext j