-- 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
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)
obtain :
  ∀ (l : 𝒰.I₀) (gi : l ⟶ i) (gj : l ⟶ j) (y : ↥(𝒰.X l))
    (hxij :
      Eq (α := ↥(𝒰.X k))
        ((𝒰.trans (P := P) fi)
            ((pullback.fst (𝒰.f i) (𝒰.f j))
                ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
              ↥(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))
                ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
              ↥(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))
                ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
              ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i)) :
          ↥X)
        ((𝒰.f j)
            ((pullback.snd (𝒰.f i) (𝒰.f j))
                ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
              ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) j)) :
          ↥X)),
    ∃ (l_1 : 𝒰.I₀) (fli : l_1 ⟶ i) (flj : l_1 ⟶ j) (x :
      Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) l_1),
      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_1)) →
                  (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))
              ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
            ↥(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_1)) →
                  (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))
              ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
            ↥(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),
    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 ⟨l, gi, gj, y, rfl⟩ := 𝒰.exists_lift_trans_eq z

Premises used: AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, rfl