-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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
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)))
this :
  ∃ (l : J) (fi : l ⟶ ↓(i, j).1) (fj : l ⟶ ↓(i, j).2) (fk : l ⟶ ↓(i, k).2) (α :
    F.obj l ⟶
      pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
        (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)))
    (z : ↥(F.obj l)),
    IsOpenImmersion α ∧
      α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
          CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
            ((F.obj ↓(i, j).1).homOfLE ⋯) ∧
        α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj ↓(i, j).1).homOfLE ⋯) ∧
          α z = x
⊢ ∃ (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)))
have obtain : ∀ (l : J) (fi : l ⟶ ↓(i, j).1) (fj : l ⟶ ↓(i, j).2) (fk : l ⟶ ↓(i, k).2)
  (α :
    F.obj l ⟶
      pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
        (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)))
  (z : ↥(F.obj l)) (hα : IsOpenImmersion α)
  (hα₁ :
    α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
      CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
        ((F.obj ↓(i, j).1).homOfLE sorry))
  (hα₂ :
    α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
      CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
        ((F.obj ↓(i, j).1).homOfLE sorry))
  (e : α z = x),
  ∃ (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)
                sorry)
              (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)
              sorry ≫
            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)
                  sorry)
                (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)
                sorry ≫
              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)
                  sorry)
                (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)
                sorry =
        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)))
Tactic: obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, e⟩ := this
Cleared hypotheses: this