-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ pullHom (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯) r r' (r ≫ a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a' (r ≫ a ≫ p' j) (r ≫ a ≫ p' j) ⋯ ⋯ ≫
        pullHom (D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯) r (r ≫ a ≫ p' j) r' ⋯ ⋯ =
    pullHom
      (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
        pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯)
      r r' r' ⋯ ⋯
have this : Eq (α :=
  Quiver.Hom (V := (↑(F.obj { as := op Z' : LocallyDiscrete Cᵒᵖ }) : Type u'))
    (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Cat.Hom.toFunctor (F.map a'.op.toLoc))
      (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₁) j))
    (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Cat.Hom.toFunctor (F.map a'.op.toLoc))
      (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₂) j)))
  (CategoryStruct.comp (Y :=
      Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (CategoryStruct.comp (Y := F.obj { as := op Z }) (F.map a.op.toLoc) (F.map r.op.toLoc)))
        (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₁) j))
      (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc sorry)))
        (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₁) j))
      (Functor.map (Cat.Hom.toFunctor (F.map r.op.toLoc))
          (Functor.map (Cat.Hom.toFunctor (F.map a.op.toLoc)) (φ.hom j)) ≫
        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc sorry)))
          (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₂) j)) :
    Quiver.Hom (V := (↑(F.obj { as := op Z' : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map a'.op.toLoc))
        (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₁) j))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map a'.op.toLoc))
        (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₂) j)))
  (Functor.map (Cat.Hom.toFunctor (F.map a'.op.toLoc)) (φ.hom j) :
    Quiver.Hom (V := (↑(F.obj { as := op Z' : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map a'.op.toLoc))
        (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₁) j))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map a'.op.toLoc))
        (obj (S := S) (f := f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₂) j)))
Tactic: have := F.mapComp'_naturality_2 a.op.toLoc r.op.toLoc a'.op.toLoc (by cat_disch) (φ.hom j)