-- 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
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)
refine_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) gi) :
          (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
            (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i))
        y :
      (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))
refine_2 :
  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) gj) :
          (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
            (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j))
        y :
      (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_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))

Tactic:
refine ⟨l, gi, gj, y, ?_, ?_⟩