-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
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₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H :
  Membership.mem (α := Sieve (Over.mk f₁)) (γ := Set (Sieve (Over.mk f₁)))
    ((J.over (X i₁) : (a : Over (X i₁)) → Set (Sieve a)) (Over.mk f₁))
    (((Sieve.overEquiv (Over.mk f₁)).symm : (a : Sieve (Over.mk f₁).left) → Sieve (Over.mk f₁))
        (Sieve.pullback q (Sieve.ofArrows X' f')) :
      Sieve (Over.mk f₁))
Y : C
j : ι'
T : C
t : T ⟶ X i₁
g : T ⟶ X' j
p : T ⟶ W
hp : p ≫ f₁ = t
fac : g ≫ f' j = p ≫ q
⊢ CategoryStruct.comp (Y :=
      Functor.obj (C := (↑(F.obj { as := op W : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map p.op.toLoc)) (Functor.obj (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (D₁.obj i₁)))
      (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' f₁.op.toLoc p.op.toLoc t.op.toLoc ⋯))) (D₁.obj i₁))
      (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
          (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁)) ≫
        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' f₁.op.toLoc p.op.toLoc t.op.toLoc ⋯))) (D₂.obj i₁)) =
    NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' f₁.op.toLoc p.op.toLoc t.op.toLoc ⋯))) (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
          (D₁.hom q f₁ f₂ ⋯ ⋯ ≫
            Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯) ≫
        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' f₁.op.toLoc p.op.toLoc t.op.toLoc ⋯))) (D₂.obj i₁)
have subst : CategoryStruct.comp (Y :=
    Functor.obj (C := (↑(F.obj { as := op W : LocallyDiscrete Cᵒᵖ }) : Type u')) (Cat.Hom.toFunctor (F.map p.op.toLoc))
      (Functor.obj (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (D₁.obj i₁)))
    (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc sorry))) (D₁.obj i₁))
    (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁)) ≫
      NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc sorry)))
        (D₂.obj i₁)) =
  NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc sorry))) (D₁.obj i₁) ≫
    Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
        (D₁.hom q f₁ f₂ sorry sorry ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ sorry sorry) ≫
      NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc sorry))) (D₂.obj i₁)
Tactic: subst hp
Cleared hypotheses: t, hp