-- 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
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (((pullFunctor F w ⋙ pullFunctor F w').obj D).obj k₁))
      (Functor.obj (C := (↑(F.obj { as := op (X'' k₂) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (obj (S := S'') (f := f'') (Functor.obj (pullFunctor F (p := r) (α := α ∘ β) (p' := r') ⋯) D) k₂)))
    (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Iso.hom
          ((fun (x : ι'') ↦
              ((Cat.Hom.toNatIso
                        (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β x)))) (q' x).op.toLoc (r' x).op.toLoc
                          ⋯)).symm.app
                  (D.obj (α (β x))) :
                Iso (C := (↑(F.obj { as := op (X'' x) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                  (Functor.obj (C := (↑(F.obj { as := op (X (α (β x))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Cat.Hom.toFunctor
                      (CategoryStruct.comp (Y := F.obj { as := op (X' (β x)) })
                        (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β x))))) (F.map (q' x).op.toLoc)))
                    (D.obj (α (β x))))
                  (Functor.obj (C := (↑(F.obj { as := op (X (α (β x))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Cat.Hom.toFunctor (F.map (r' x).op.toLoc)) (D.obj (α (β x))))))
            k₁)) ≫
      hom (Functor.obj (pullFunctor F (p := r) (α := α ∘ β) (p' := r') ⋯) D) s f₁ f₂ ⋯ ⋯)
    (((pullFunctor F w ⋙ pullFunctor F w').obj D).hom s f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Iso.hom
          ((fun (x : ι'') ↦
              ((Cat.Hom.toNatIso
                        (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β x)))) (q' x).op.toLoc (r' x).op.toLoc
                          ⋯)).symm.app
                  (D.obj (α (β x))) :
                Iso (C := (↑(F.obj { as := op (X'' x) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                  (Functor.obj (C := (↑(F.obj { as := op (X (α (β x))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Cat.Hom.toFunctor
                      (CategoryStruct.comp (Y := F.obj { as := op (X' (β x)) })
                        (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β x))))) (F.map (q' x).op.toLoc)))
                    (D.obj (α (β x))))
                  (Functor.obj (C := (↑(F.obj { as := op (X (α (β x))) : LocallyDiscrete Cᵒᵖ }) : Type u'))
                    (Cat.Hom.toFunctor (F.map (r' x).op.toLoc)) (D.obj (α (β x))))))
            k₂)))
have dsimp : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
      ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₁)))) (q' k₁).op.toLoc (r' k₁).op.toLoc
                sorry).inv.toNatTrans.app
        (D.obj (α (β k₁)))) ≫
    pullFunctorObjHom (p := r) sorry D (f₁ ≫ f'' k₁) f₁ f₂ sorry sorry =
  pullFunctorObjHom w' (pullFunctorObj w D) (f₁ ≫ f'' k₁) f₁ f₂ sorry sorry ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
      ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₂)))) (q' k₂).op.toLoc (r' k₂).op.toLoc
                sorry).inv.toNatTrans.app
        (D.obj (α (β k₂))))
Tactic: dsimp