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 : 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₂))
e_a :
  Eq (α := (pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).Hom (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)
    ((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)
⊢ 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:
congr 5
-- 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 : 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 (α := (pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).Hom (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)
    ((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)

Tactic:
simpa using congr($(pullback.condition (f := (F.obj i).homOfLE h₁)
        (g := (F.obj i).homOfLE h₂)) ≫ Scheme.Opens.ι _)

Premises used: AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Limits.pullback.condition
-- 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 : 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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
⊢ (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ≫
      (F.obj i).homOfLE h₁ =
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ≫
      (F.obj i).homOfLE h₂

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _), ← Functor.map_comp,
        Subsingleton.elim (hli ≫ k₁.2.1) (hlj ≫ k₂.2.1)]

Premises used: CategoryTheory.cancel_mono, Prod.fst, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Functor.map_comp, Subsingleton.elim, Sigma.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
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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
simp :
  IsOpenImmersion (Y := (↑(Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme))
    (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
⊢ IsOpenImmersion (α ≫ pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))

Tactic:
simp only [pullback.lift_fst, α]

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

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
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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
⊢ IsOpenImmersion (α ≫ pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))

Tactic:
have : IsOpenImmersion (α ≫ pullback.fst _ _) := by
      simp only [pullback.lift_fst, α]; 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
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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
this : IsOpenImmersion (α ≫ pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ IsOpenImmersion α

Tactic:
.of_comp _ (pullback.fst _ _)

Premises used: CategoryTheory.Limits.pullback.fst, 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
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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
this : IsOpenImmersion (α ≫ pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ IsOpenImmersion α

Tactic:
exact .of_comp _ (pullback.fst _ _)
-- 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 : 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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
⊢ IsOpenImmersion α

Tactic:
have : IsOpenImmersion α := by
    have : IsOpenImmersion (α ≫ pullback.fst _ _) := by
      simp only [pullback.lift_fst, α]; infer_instance
    exact .of_comp _ (pullback.fst _ _)
-- 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 : 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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ 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)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
this : IsOpenImmersion α
⊢ α y = x

Tactic:
have : α y = x := by
    simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map, Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.comp_apply] at hy₁
    apply (pullback.fst ((F.obj i).homOfLE h₁) _).isOpenEmbedding.injective
    simp only [← Scheme.Hom.comp_apply, α, pullback.lift_fst]
    simp_all