awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
simp :
  Iso.inv (Hom.isoOpensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)) ≫
      F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).2 =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
        k ≫
      Opens.ι
        (⨆ (k : (k : J) × (k ⟶ i) × (k ⟶ i)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1))
⊢ PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
        k ≫
      t F i i =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
        k ≫
      𝟙 (↑(V F i i) : Scheme)

Tactic:
simp only [Category.comp_id, ← cancel_mono (Scheme.Opens.ι _), Category.assoc,
    IsOpenImmersion.lift_fac, Scheme.Cover.ι_glueMorphisms, t, tAux, V]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.tAux, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.t, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.IsLocallyDirected.V, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- 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
i : J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
⊢ Iso.inv (Hom.isoOpensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)) ≫
      F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).2 =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
        k ≫
      Opens.ι
        (⨆ (k : (k : J) × (k ⟶ i) × (k ⟶ i)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1))

Tactic:
simp [Scheme.Opens.iSupOpenCover, Iso.inv_comp_eq, Subsingleton.elim k.2.1 k.2.2]

Premises used: CategoryTheory.Iso.inv_comp_eq, Prod.fst, AlgebraicGeometry.Scheme.Opens.iSupOpenCover, Subsingleton.elim, Sigma.snd, Prod.snd
-- 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)))
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 ⋯))
    (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 ⋯)),
    Membership.mem (α := ↥(F.obj ↓j)) (γ := Set ↥(F.obj ↓j))
      (Set.range (ι := ↥(↑(V F (↓(j, k).1) ↓(j, k).2) : Scheme)) ⇑(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)
          (α z :
            ↥(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)))) :
        ↥(F.obj ↓j))
⊢ Membership.mem (α := ↥(F.obj ↓j)) (γ := Set ↥(F.obj ↓j))
    (Set.range (ι := ↥(↑(V F (↓(j, k).1) ↓(j, k).2) : Scheme)) ⇑(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) x :
      ↥(F.obj ↓j))

Tactic:
obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, rfl⟩ := exists_of_pullback_V_V F x

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, rfl
-- 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
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 ⋯)
rw : Membership.mem (α := ↥(F.obj ↓j)) (γ := (F.obj ↓j).Opens) (V F (↓j) ↓k) ((F.map fj) z : ↥(F.obj ↓j))
⊢ Membership.mem (α := ↥(F.obj ↓j)) (γ := Set ↥(F.obj ↓j))
    (Set.range (ι := ↥(↑(V F (↓(j, k).1) ↓(j, k).2) : Scheme)) ⇑(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)
        (α z :
          ↥(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)))) :
      ↥(F.obj ↓j))

Tactic:
rw [← Scheme.Hom.comp_apply, reassoc_of% hα₁, homOfLE_tAux F ↓i ↓j fi fj,
        Iso.hom_inv_id_assoc, Scheme.Opens.range_ι, SetLike.mem_coe]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.Scheme.Hom.comp_apply, SetLike.mem_coe, CategoryTheory.Iso.hom_inv_id_assoc, AlgebraicGeometry.Scheme.Opens.range_ι, Equiv.symm, equivShrink, DFunLike.coe
-- 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
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 ⋯)
⊢ Membership.mem (α := ↥(F.obj ↓j)) (γ := (F.obj ↓j).Opens) (V F (↓j) ↓k) ((F.map fj) z : ↥(F.obj ↓j))

Tactic:
TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨l, fj, fk⟩, ⟨z, rfl⟩⟩

Premises used: Iff.mpr, Set.Mem, Prod.mk, TopologicalSpace.Opens.mem_iSup, Exists.intro, Sigma.mk, rfl
-- 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
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 ⋯)
⊢ Membership.mem (α := ↥(F.obj ↓j)) (γ := (F.obj ↓j).Opens) (V F (↓j) ↓k) ((F.map fj) z : ↥(F.obj ↓j))

Tactic:
exact TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨l, fj, fk⟩, ⟨z, rfl⟩⟩
-- 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
⊢ Eq (α :=
    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)) ⟶
      F.obj ↓j)
    (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) ⋯ ≫
      Opens.ι (V F (↓(j, k).1) ↓(j, k).2))
    ((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) ≫
      Opens.ι (V F (↓(j, i).1) ↓(j, i).2))

Tactic:
simp [t]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.t
-- 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
⊢ 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:
Scheme.hom_ext_of_forall _ _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.hom_ext_of_forall
-- 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)),
    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

Tactic:
have := exists_of_pullback_V_V F x
-- 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
⊢ ∃ (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)))

Tactic:
⟨α.opensRange, ⟨_, e⟩, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, And.intro, Exists.intro
-- 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
rw :
  (Hom.opensRange α).ι ≫
      IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
          (CategoryStruct.comp (Y :=
            pullback (X := (↑(V F (↓j) ↓k) : Scheme)) (Y := (↑(V F (↓j) ↓i) : Scheme)) (Opens.ι (V F (↓j) ↓k))
              (Opens.ι (V F (↓j) ↓i)))
            (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) ⋯)
              ⋯)
            (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)
⊢ (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)

Tactic:
rw [IsOpenImmersion.comp_lift_assoc]

Premises used: AlgebraicGeometry.IsOpenImmersion.comp_lift_assoc
-- 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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (Hom.opensRange α).ι ≫
      IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
          (CategoryStruct.comp (Y :=
            pullback (X := (↑(V F (↓j) ↓k) : Scheme)) (Y := (↑(V F (↓j) ↓i) : Scheme)) (Opens.ι (V F (↓j) ↓k))
              (Opens.ι (V F (↓j) ↓i)))
            (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) ⋯)
              ⋯)
            (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)

Tactic:
simp only [limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.cospan_left, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc