-- 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
pf : IsOpenImmersion (X := (↑(V F (↓j) ↓k) : Scheme)) (Opens.ι (V F (↓j) ↓k))
h₁ :
  Subset (α := Set ↥(F.obj ↓j)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fj))
    (Set.range (ι := ↥(↑(V F (↓j) ↓k) : Scheme)) ⇑(Opens.ι (V F (↓j) ↓k)))
pf_1 : IsOpenImmersion (X := (↑(V F (↓k) ↓i) : Scheme)) (Opens.ι (V F (↓k) ↓i))
pf_2 :
  Subset (α := Set ↥(F.obj ↓k))
    (Set.range (ι := ↥(F.obj l)) ⇑(IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ ≫ tAux F (↓j) ↓k))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
pf_3 : IsOpenImmersion (F.map fi)
pf_4 :
  ∀ (k_1 : (k_1 : J) × (k_1 ⟶ ↓i) × (k_1 ⟶ ↓k)),
    IsOpenImmersion (F.map k_1.snd (β := fun (k_2 : J) ↦ (k_2 ⟶ ↓i) × (k_2 ⟶ ↓k)).1)
pf_5 : Hom.opensRange (F.map fi) ≤ V F (↓i) ↓k
this_1 :
  IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fj)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fj)))
      ((F.obj ↓j).homOfLE ⋯)
h₂ :
  Subset (α := Set ↥(F.obj ↓k)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fk))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
this :
  IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) h₂ =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fk)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fk)))
      ((F.obj ↓k).homOfLE ⋯)
simp_rw : (Hom.opensRange (F.map fi)).ι = (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)
⊢ IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) h₂ ≫ tAux F (↓k) ↓i =
    Iso.hom (Hom.isoOpensRange (F.map fi)) ≫ (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)

Tactic:
simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fk fi, Iso.hom_inv_id_assoc,
      ← Iso.inv_comp_eq, Scheme.Hom.isoOpensRange_inv_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, CategoryTheory.Iso.hom_inv_id_assoc, AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp