-- 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
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))
have 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) sorry) 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) sorry) 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) sorry) 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) sorry) 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) sorry) 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) sorry) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(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
Cleared hypotheses: z, hxij, this