-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (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
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
              ((F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
            (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (obj' i₂)
have rw : CategoryStruct.comp (Y :=
    Functor.obj (C := (↑(F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (obj i₁)))
    (NatTrans.app
      (Cat.Hom₂.toNatTrans
        (Iso.hom
          (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)
            gf₁.op.toLoc sorry)))
      (obj i₁))
    (NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.hom
            (F.mapComp' p.op.toLoc g.op.toLoc
              (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) sorry)))
        (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (obj i₁)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂)) ≫
        NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (F.mapComp' p.op.toLoc g.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) sorry)))
            (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (obj' i₂)) ≫
          NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.inv
                (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)
                  gf₂.op.toLoc sorry)))
            (obj' i₂)) =
  (F.mapComp' (sq i₁ i₂).p₁.op.toLoc
              (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
              sorry).hom.toNatTrans.app
      (obj i₁) ≫
    Functor.map
        (Cat.Hom.toFunctor
          (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
        (hom i₁ i₂) ≫
      (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                sorry).inv.toNatTrans.app
        (obj' i₂)
Tactic: rw [F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
    _ _ _ _ _ _ (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst])
    rfl (by cat_disch),
    F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app _ _ _ _ _ _
      (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]) rfl (by cat_disch)]