-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1_1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2_1 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
xk : ↥(d.functor.obj k)
h1 : (d.functor.map fj) xk = xj
h2 : (d.natTrans.app k) xk = uk
⊢ Eq (α := ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    ((pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
        ((pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) xk :
          ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))) :
      ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    ((pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
        x :
      ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
have h : Eq (α := ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
  ((CategoryStruct.comp (Y :=
        pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
        (pullback.lift (d.functor.map fi) (d.functor.map fj) sorry)
        (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j)))
      xk :
    ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
  ((pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
      x :
    ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
Tactic: rw [← Scheme.Hom.comp_apply]