-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
refine :
  ∀
    (x :
      ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
          (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))),
    ∃ (U :
      (pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
          (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2))).Opens),
      x ∈ U ∧
        U.ι ≫
            pullback.lift
                (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
                  (pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)) ≫
                    tAux F (↓i) ↓j)
                  ⋯)
                (pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)) ≫
                  t F (↓(i, j).1) ↓(i, j).2)
                ⋯ ≫
              pullback.lift
                  (IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
                    (pullback.fst (Opens.ι (V F (↓(j, k).1) ↓(j, k).2)) (Opens.ι (V F (↓(j, i).1) ↓(j, i).2)) ≫
                      tAux F (↓j) ↓k)
                    ⋯)
                  (pullback.fst (Opens.ι (V F (↓(j, k).1) ↓(j, k).2)) (Opens.ι (V F (↓(j, i).1) ↓(j, i).2)) ≫
                    t F (↓(j, k).1) ↓(j, k).2)
                  ⋯ ≫
                pullback.lift
                  (IsOpenImmersion.lift (Opens.ι (V F (↓i) ↓j))
                    (pullback.fst (Opens.ι (V F (↓(k, i).1) ↓(k, i).2)) (Opens.ι (V F (↓(k, j).1) ↓(k, j).2)) ≫
                      tAux F (↓k) ↓i)
                    ⋯)
                  (pullback.fst (Opens.ι (V F (↓(k, i).1) ↓(k, i).2)) (Opens.ι (V F (↓(k, j).1) ↓(k, j).2)) ≫
                    t F (↓(k, i).1) ↓(k, i).2)
                  ⋯ =
          U.ι ≫
            𝟙
              (pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
                (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
⊢ pullback.lift
        (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
          (pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)) ≫ tAux F (↓i) ↓j) ⋯)
        (pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)) ≫
          t F (↓(i, j).1) ↓(i, j).2)
        ⋯ ≫
      pullback.lift
          (IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
            (pullback.fst (Opens.ι (V F (↓(j, k).1) ↓(j, k).2)) (Opens.ι (V F (↓(j, i).1) ↓(j, i).2)) ≫ tAux F (↓j) ↓k)
            ⋯)
          (pullback.fst (Opens.ι (V F (↓(j, k).1) ↓(j, k).2)) (Opens.ι (V F (↓(j, i).1) ↓(j, i).2)) ≫
            t F (↓(j, k).1) ↓(j, k).2)
          ⋯ ≫
        pullback.lift
          (IsOpenImmersion.lift (Opens.ι (V F (↓i) ↓j))
            (pullback.fst (Opens.ι (V F (↓(k, i).1) ↓(k, i).2)) (Opens.ι (V F (↓(k, j).1) ↓(k, j).2)) ≫ tAux F (↓k) ↓i)
            ⋯)
          (pullback.fst (Opens.ι (V F (↓(k, i).1) ↓(k, i).2)) (Opens.ι (V F (↓(k, j).1) ↓(k, j).2)) ≫
            t F (↓(k, i).1) ↓(k, i).2)
          ⋯ =
    𝟙
      (pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
        (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))

Tactic:
refine Scheme.hom_ext_of_forall _ _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.hom_ext_of_forall