-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
obtain :
  ∀ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (G ⋙ forget).obj l)
    (hi :
      Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
              (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
            x :
          (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        ((s.app i) xi : ↥(G.obj i)))
    (hj :
      Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
              (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
            x :
          (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        ((s.app j) xj : ↥(G.obj j))),
    ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (F ⋙ forget).obj l),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
            x =
          xi ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
            x =
          xj
⊢ ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj

Tactic:
obtain ⟨l, fli, flj, x, hi, hj⟩ := (G ⋙ Scheme.forget).exists_map_eq_of_isLocallyDirected fi fj
        (s.app i xi) (s.app j xj) <| by
      simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      dsimp at heq
      rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]
      simp

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.forget, CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.NatTrans.app