-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
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)
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))
⊢ ∃ (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

Tactic:
obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj this

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, rfl