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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
y₁ : ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))
hy₁ :
  Eq (α := ↥(F.obj i)) ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) y₁ : ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
obtain :
  ∀ (k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)) (y₂ : ↥(F.obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)))))
    (hy₂ :
      Eq (α := ↥(F.obj i)) ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1) y₂ : ↥(F.obj i))
        ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))),
    ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)),
      IsOpenImmersion α ∧
        α ≫ pullback.fst (V F i j).ι (V F i k).ι =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj i).homOfLE ⋯) ∧
          α ≫ pullback.snd (V F i j).ι (V F i k).ι =
              CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme))
                (Iso.hom (Hom.isoOpensRange (F.map fi))) ((F.obj i).homOfLE ⋯) ∧
            α z = x
⊢ ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)),
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι =
          CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
            ((F.obj i).homOfLE ⋯) ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj i).homOfLE ⋯) ∧
          α z = x

Tactic:
obtain ⟨k₂, y₂, hy₂⟩ := mem_iSup.mp ((pullback.snd (C := Scheme) _ _) x).2

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.mem_iSup, Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, Subtype.property
-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
y₁ : ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))
hy₁ :
  Eq (α := ↥(F.obj i)) ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) y₁ : ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
y₂ : ↥(F.obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))
hy₂ :
  Eq (α := ↥(F.obj i)) ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1) y₂ : ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
⊢ Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
        y₁ :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙ forget).map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
        y₂ :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))

Tactic:
simpa [hy₁, hy₂] using congr($(pullback.condition (f := (V F i j).ι)) 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
⊢ CategoryStruct.comp (Y :=
        (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
        (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
        ((F.obj i).homOfLE ⋯) ≫
      (V F i j).ι =
    CategoryStruct.comp (Y :=
        (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
        (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
        ((F.obj i).homOfLE ⋯) ≫
      (V F i k).ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst_1 : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_3 : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
inst : IsOpenImmersion (X := pullback (V F i j).ι (V F i k).ι) (pullback.fst (V F i j).ι (V F i k).ι)
inst₁ : IsOpenImmersion (α ≫ pullback.fst (V F i j).ι (V F i k).ι)
Z : Scheme
g : pullback (V F i j).ι (V F i k).ι ⟶ (↑(V F i j) : Scheme)
⊢ IsOpenImmersion α

Tactic:
apply +allowSynthFailures IsOpenImmersion.of_comp

Premises used: AlgebraicGeometry.IsOpenImmersion.of_comp
-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
⊢ IsOpenImmersion (X := pullback (V F i j).ι (V F i k).ι) (pullback.fst (V F i j).ι (V F i k).ι)

Tactic:
(inferInstance : IsOpenImmersion (pullback.fst (V F i j).ι (V F i k).ι))

Premises used: inferInstance
-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
⊢ IsOpenImmersion (X := pullback (V F i j).ι (V F i k).ι) (pullback.fst (V F i j).ι (V F i k).ι)

Tactic:
exact (inferInstance : IsOpenImmersion (pullback.fst (V F i j).ι (V F i k).ι))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst_1 : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_3 : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
inst :
  IsOpenImmersion (Y := (↑(V F i j) : Scheme))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
⊢ IsOpenImmersion (α ≫ pullback.fst (V F i j).ι (V F i k).ι)

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

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
⊢ IsOpenImmersion (Y := (↑(V F i j) : Scheme))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))

Tactic:
infer_instance
-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
⊢ IsOpenImmersion α

Tactic:
have : IsOpenImmersion α := by
    apply +allowSynthFailures IsOpenImmersion.of_comp
    · exact (inferInstance : IsOpenImmersion (pullback.fst (V F i j).ι (V F i k).ι))
    · simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, α]
      infer_instance
-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))
z : (F ⋙ forget).obj l
hy₁ :
  Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
hy₂ :
  Eq (α := ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
            z :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
      ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
this : IsOpenImmersion α
a :
  Eq (α := ↥(↑(V F i j) : Scheme)) ((pullback.fst (V F i j).ι (V F i k).ι) (α z) : ↥(↑(V F i j) : Scheme))
    ((pullback.fst (V F i j).ι (V F i k).ι) x : ↥(↑(V F i j) : Scheme))
⊢ α z = x

Tactic:
apply (pullback.fst (C := Scheme) _ _).isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective