awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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
⊢ IsOpenImmersion α
have g : pullback (V F i j).ι (V F i k).ι ⟶ (↑(V F i j) : Scheme)
Tactic: apply +allowSynthFailures IsOpenImmersion.of_comp
-- 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
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 (α ≫ pullback.fst (V F i j).ι (V F i k).ι)
have 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 sorry))
Tactic: simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, α]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
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 ⋯))
    ⋯
⊢ ∃ (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
have this : 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
-- 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
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 α
⊢ α z = x
have 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))
Tactic: apply (pullback.fst (C := Scheme) _ _).isOpenEmbedding.injective
-- 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
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 α
⊢ 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))
have a : Eq (α := ↥(F.obj i)) ((V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) (α z) : ↥(↑(V F i j) : Scheme)) : ↥(F.obj i))
  ((V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x : ↥(↑(V F i j) : Scheme)) : ↥(F.obj i))
Tactic: apply (V F i j).ι.isOpenEmbedding.injective
-- 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
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 α
⊢ Eq (α := ↥(F.obj i))
    ((V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) (α z) : ↥(↑(V F i j) : Scheme)) : ↥(F.obj i))
    ((V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x : ↥(↑(V F i j) : Scheme)) : ↥(F.obj i))
have a : Eq (α := ↥(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 sorry) ≫
        (V F i j).ι)
      z :
    ↥(F.obj i))
  ((V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x : ↥(↑(V F i j) : Scheme)) : ↥(F.obj i))
Tactic: rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.lift_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
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 α
⊢ ∃ (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
have this₁ : α z = x
Tactic: have : α z = x := by
    apply (pullback.fst (C := Scheme) _ _).isOpenEmbedding.injective
    apply (V F i j).ι.isOpenEmbedding.injective
    rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.lift_fst_assoc]
    simpa using hy₁
-- 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
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
⊢ Eq (α := pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ⟶ F.obj j)
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
      Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
        F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2)
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
      Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
        F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2)
have H : ∀ (x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))),
  ∃ (U_1 : (pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).Opens),
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
              F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
              F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2
Tactic: apply Scheme.hom_ext_of_forall
-- 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
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ Eq (α := ↥(F.obj i))
    ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((TopCat.Hom.hom
                (Hom.base
                  (LocallyRingedSpace.Hom.toHom
                    (Hom.toLRSHom'
                      (Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
              (a : ↥(↑(Hom.opensRange (F.map k₁.snd.1)) : Scheme)) → ↥(F.obj k₁.fst))
            ((TopCat.Hom.hom
                    (Hom.base
                      (LocallyRingedSpace.Hom.toHom
                        (Hom.toLRSHom' (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))))) :
                  (a : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))) →
                    ↥(↑(Hom.opensRange (F.map k₁.snd.1)) : Scheme))
                x :
              ↥(↑(Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme)) :
          ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
    ((F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
        ((TopCat.Hom.hom
                (Hom.base
                  (LocallyRingedSpace.Hom.toHom
                    (Hom.toLRSHom'
                      (Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
              (a : ↥(↑(Hom.opensRange (F.map k₂.snd.1)) : Scheme)) → ↥(F.obj k₂.fst))
            ((TopCat.Hom.hom
                    (Hom.base
                      (LocallyRingedSpace.Hom.toHom
                        (Hom.toLRSHom' (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))))) :
                  (a : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))) →
                    ↥(↑(Hom.opensRange (F.map k₂.snd.1)) : Scheme))
                x :
              ↥(↑(Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme)) :
          ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj i))
have simp : Eq (α := ↥(F.obj i))
  (((pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ≫
        F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
      x :
    ↥(F.obj i))
  (((pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ≫
        F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
      x :
    ↥(F.obj i))
Tactic: simp only [← Hom.comp_apply]