-- 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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app
        (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.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc
                      (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc
                        f₁.op.toLoc)
                      ⋯).inv.toNatTrans.app
              (D.obj (α j₁)) ≫
            D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
              (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc
                        (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc
                          f₂.op.toLoc)
                        ⋯).hom.toNatTrans.app
                (D.obj (α j₂))) ≫
        (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app
          (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₂))) =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc
                (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc gf₁.op.toLoc)
                ⋯).inv.toNatTrans.app
        (D.obj (α j₁)) ≫
      ((F.mapComp' (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc f₁.op.toLoc)
                    g.op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc
                      gf₁.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D.obj (α j₁)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc)) (D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯) ≫
            (F.mapComp'
                      (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc
                        f₂.op.toLoc)
                      g.op.toLoc
                      (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc
                        gf₂.op.toLoc)
                      ⋯).inv.toNatTrans.app
              (D.obj (α j₂))) ≫
        (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc gf₂.op.toLoc)
                  ⋯).hom.toNatTrans.app
          (D.obj (α j₂))
have simp : Eq (α :=
  Quiver.Hom (V := (↑(F.obj { as := op Y' : LocallyDiscrete Cᵒᵖ }) : Type u'))
    (Functor.obj (C := (↑(F.obj { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Cat.Hom.toFunctor (F.map gf₁.op.toLoc))
      (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 gf₂.op.toLoc))
      (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₂)))))
  ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc sorry).hom.toNatTrans.app
      (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.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
        ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₁) }) (p' j₁).op.toLoc f₁.op.toLoc) sorry).inv.toNatTrans.app
          (D.obj (α j₁))) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc)) (D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) sorry sorry) ≫
        Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
            ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc
                      (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc
                        f₂.op.toLoc)
                      sorry).hom.toNatTrans.app
              (D.obj (α j₂))) ≫
          (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc sorry).inv.toNatTrans.app
            (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₂))))
  ((F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc
              (CategoryStruct.comp (Y := { as := op (X' j₁) }) (p' j₁).op.toLoc gf₁.op.toLoc) sorry).inv.toNatTrans.app
      (D.obj (α j₁)) ≫
    (F.mapComp' (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc f₁.op.toLoc)
                g.op.toLoc
                (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc gf₁.op.toLoc)
                sorry).hom.toNatTrans.app
        (D.obj (α j₁)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc)) (D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) sorry sorry) ≫
        (F.mapComp' (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc f₂.op.toLoc)
                    g.op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc
                      gf₂.op.toLoc)
                    sorry).inv.toNatTrans.app
            (D.obj (α j₂)) ≫
          (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc
                      gf₂.op.toLoc)
                    sorry).hom.toNatTrans.app
            (D.obj (α j₂)))
Tactic: simp only [Functor.map_comp, Category.assoc]