-- 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
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)))
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 ⋯)
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 ⋯)
e : α z = x
simp :
  (Hom.opensRange α).ι ≫
      pullback.lift
          (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
            (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ tAux F (↓i) ↓j) ⋯)
          (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫
            IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓i)) (tAux F (↓i) ↓j) ⋯)
          ⋯ ≫
        IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
            (pullback.fst (Opens.ι (V F (↓j) ↓k)) (Opens.ι (V F (↓j) ↓i)) ≫ tAux F (↓j) ↓k) ⋯ ≫
          tAux F (↓k) ↓i =
    (Hom.opensRange α).ι ≫ pullback.snd (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ Opens.ι (V F (↓i) ↓k)
⊢ CategoryStruct.comp (Y :=
        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)))
        ((Hom.opensRange α).ι ≫
          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.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2))) ≫
      Opens.ι (V F (↓(i, k).1) ↓(i, k).2) =
    (((Hom.opensRange α).ι ≫
          𝟙
            (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.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2))) ≫
      Opens.ι (V F (↓(i, k).1) ↓(i, k).2)

Tactic:
simp only [t, Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
      limit.lift_π_assoc, cospan_left, IsOpenImmersion.lift_fac, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.cospan_left, AlgebraicGeometry.Scheme.IsLocallyDirected.t, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π, AlgebraicGeometry.IsOpenImmersion.lift_fac, CategoryTheory.Category.id_comp