-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i
xj : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) j
hxij : Eq (α := ↥(𝒰.X k)) ((𝒰.trans (P := P) fi) xi : ↥(𝒰.X k)) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k))
this : Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
⊢ ∃ (l : 𝒰.I₀) (fli : l ⟶ i) (flj : l ⟶ j) (x :
    Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) l),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) fli) :
            (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
              (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) flj) :
            (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
              (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j))
          x =
        xj
have obtain : ∀ (z : ↥(pullback (𝒰.f i) (𝒰.f j)))
  (hxij :
    Eq (α := ↥(𝒰.X k))
      ((𝒰.trans (P := P) fi)
          ((pullback.fst (𝒰.f i) (𝒰.f j)) z :
            ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i)) :
        ↥(𝒰.X k))
      ((𝒰.trans (P := P) fj)
          ((pullback.snd (𝒰.f i) (𝒰.f j)) z :
            ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) j)) :
        ↥(𝒰.X k)))
  (this :
    Eq (α := ↥X)
      ((𝒰.f i)
          ((pullback.fst (𝒰.f i) (𝒰.f j)) z :
            ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i)) :
        ↥X)
      ((𝒰.f j)
          ((pullback.snd (𝒰.f i) (𝒰.f j)) z :
            ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) j)) :
        ↥X)),
  ∃ (l : 𝒰.I₀) (fli : l ⟶ i) (flj : l ⟶ j) (x :
    Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) l),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) fli) :
              (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
                (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i))
        ((pullback.fst (𝒰.f i) (𝒰.f j)) z :
          ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i)) ∧
      Eq (α :=
        (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) j))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) flj) :
              (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
                (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) j))
        ((pullback.snd (𝒰.f i) (𝒰.f j)) z : ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) j))
Tactic: obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj this
Cleared hypotheses: xi, xj, hxij, this