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
inst_4 : Small.{u, w} J
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
mp :
  (∃ (x : ↥((glueData F).V (i, j))), ((glueData F).f i j) x = xi ∧ ((glueData F).t i j ≫ (glueData F).f j i) x = xj) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj
⊢ GlueData.Rel.{u} (glueData F) (Sigma.mk (β := fun (i : (glueData F).J) ↦ ↥((glueData F).U i)) i xi)
      (Sigma.mk (β := fun (i : (glueData F).J) ↦ ↥((glueData F).U i)) j xj) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
dsimp +instances only [GlueData.Rel]

Premises used: AlgebraicGeometry.Scheme.GlueData.Rel
-- 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
mp :
  ∀ (k : J) (ki : k ⟶ ↓(i, j).1) (kj : k ⟶ ↓(i, j).2)
    (y :
      ↥(F.obj
          (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
            (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) k (ki, kj)))))
    (hy :
      Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))),
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x_1 : ↥(F.obj k)),
      Eq (α := ↥(F.obj ↓i)) ((F.map fi) x_1 : ↥(F.obj ↓i)) (((glueData F).f i j) x : ↥((glueData F).U i)) ∧
        Eq (α := ↥(F.obj ↓j)) ((F.map fj) x_1 : ↥(F.obj ↓j))
          (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))
⊢ ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x_1 : ↥(F.obj k)),
    Eq (α := ↥(F.obj ↓i)) ((F.map fi) x_1 : ↥(F.obj ↓i)) (((glueData F).f i j) x : ↥((glueData F).U i)) ∧
      Eq (α := ↥(F.obj ↓j)) ((F.map fj) x_1 : ↥(F.obj ↓j))
        (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))

Tactic:
obtain ⟨⟨k, ki, kj⟩, y, hy : F.map ki y = (glueData F).f i j x⟩ := mem_iSup.mp x.2

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, CategoryTheory.GlueData.f, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.mem_iSup, Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.GlueData.toGlueData, 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
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : J
ki : k ⟶ ↓(i, j).1
kj : k ⟶ ↓(i, j).2
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) k (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
⊢ ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x_1 : ↥(F.obj k)),
    Eq (α := ↥(F.obj ↓i)) ((F.map fi) x_1 : ↥(F.obj ↓i)) (((glueData F).f i j) x : ↥((glueData F).U i)) ∧
      Eq (α := ↥(F.obj ↓j)) ((F.map fj) x_1 : ↥(F.obj ↓j))
        (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))

Tactic:
⟨k, ki, kj, y, hy, ?_⟩

Premises used: 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : J
ki : k ⟶ ↓(i, j).1
kj : k ⟶ ↓(i, j).2
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) k (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
mp :
  Eq (α := ↥(F.obj ↓j)) ((F.map kj) y : ↥(F.obj ↓j)) (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))
⊢ ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x_1 : ↥(F.obj k)),
    Eq (α := ↥(F.obj ↓i)) ((F.map fi) x_1 : ↥(F.obj ↓i)) (((glueData F).f i j) x : ↥((glueData F).U i)) ∧
      Eq (α := ↥(F.obj ↓j)) ((F.map fj) x_1 : ↥(F.obj ↓j))
        (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))

Tactic:
refine ⟨k, ki, kj, y, hy, ?_⟩
-- 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : J
ki : k ⟶ ↓(i, j).1
kj : k ⟶ ↓(i, j).2
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) k (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
mp :
  ∀ (k : Shrink.{u, w} J) (ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J))
    (kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J))
    (y :
      ↥(F.obj
          (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
            (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj)))))
    (hy :
      Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))),
    Eq (α := ↥(F.obj ↓j)) ((F.map kj) y : ↥(F.obj ↓j))
      (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))
⊢ Eq (α := ↥(F.obj ↓j)) ((F.map kj) y : ↥(F.obj ↓j)) (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))

Tactic:
obtain ⟨k, rfl⟩ := (equivShrink J).symm.surjective k

Premises used: Equiv.surjective, Equiv.symm, equivShrink, 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
mp :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((glueData F).ι j) (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j)) : ↥(glueData F).glued)
⊢ Eq (α := ↥(F.obj ↓j)) ((F.map kj) y : ↥(F.obj ↓j)) (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j))

Tactic:
apply ((glueData F).ι _).isOpenEmbedding.injective

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective
-- 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
mp :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((glueData F).ι j) (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j)) : ↥(glueData F).glued)

Tactic:
simp only [← Scheme.Hom.comp_apply, Category.assoc, GlueData.glue_condition]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
trans :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((glueData F).ι k) y : ↥(glueData F).glued)
trans₁ :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι k) y : ↥(glueData F).glued)
    (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)

Tactic:
trans (glueData F).ι k y

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
simp :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((glueData F).ι j)))) :
            C(↥(F.obj ↓j), ↥(glueData F).glued)) :
          (a : ↥(F.obj ↓j)) → ↥(glueData F).glued)
        ((TopCat.Hom.hom (F.map kj).base : (a : ↥((glueData F).U k)) → ↥(F.obj ↓j)) y : ↥(F.obj ↓j)) :
      ↥(glueData F).glued)
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((glueData F).ι k) y : ↥(glueData F).glued)

Tactic:
simp [← glueDataι_naturality F kj]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality
-- 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι j) ((F.map kj) y : ↥(F.obj ↓j)) : ↥(glueData F).glued)
    (((TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((glueData F).ι j)))) :
            C(↥(F.obj ↓j), ↥(glueData F).glued)) :
          (a : ↥(F.obj ↓j)) → ↥(glueData F).glued)
        ((TopCat.Hom.hom (F.map kj).base : (a : ↥((glueData F).U k)) → ↥(F.obj ↓j)) y : ↥(F.obj ↓j)) :
      ↥(glueData F).glued)

Tactic:
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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
simp :
  Eq (α := ↥(glueData F).glued)
    (((TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((glueData F).ι i)))) :
            C(↥(F.obj ↓i), ↥(glueData F).glued)) :
          (a : ↥(F.obj ↓i)) → ↥(glueData F).glued)
        ((TopCat.Hom.hom (F.map ki).base : (a : ↥((glueData F).U k)) → ↥(F.obj ↓i)) y : ↥(F.obj ↓i)) :
      ↥(glueData F).glued)
    ((TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((glueData F).ι i)))) :
          (a : ↥((glueData F).U i)) → ↥(glueData F).glued)
        ((F.map ki) y : ↥(F.obj ↓i)) :
      ↥(glueData F).glued)
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι k) y : ↥(glueData F).glued)
    (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)

Tactic:
simp [← glueDataι_naturality F ki, ← hy]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality
-- 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 : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).1 : J)
kj : Quiver.Hom.{v, w} (V := J) (↓k : J) (↓(i, j).2 : J)
y :
  ↥(F.obj
      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2))
        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓(i, j).1) × (k ⟶ ↓(i, j).2)) (↓k) (ki, kj))))
hy : Eq (α := ↥(F.obj ↓(i, j).1)) ((F.map ki) y : ↥(F.obj ↓(i, j).1)) (((glueData F).f i j) x : ↥((glueData F).U i))
⊢ Eq (α := ↥(glueData F).glued)
    (((TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((glueData F).ι i)))) :
            C(↥(F.obj ↓i), ↥(glueData F).glued)) :
          (a : ↥(F.obj ↓i)) → ↥(glueData F).glued)
        ((TopCat.Hom.hom (F.map ki).base : (a : ↥((glueData F).U k)) → ↥(F.obj ↓i)) y : ↥(F.obj ↓i)) :
      ↥(glueData F).glued)
    ((TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((glueData F).ι i)))) :
          (a : ↥((glueData F).U i)) → ↥(glueData F).glued)
        ((F.map ki) y : ↥(F.obj ↓i)) :
      ↥(glueData F).glued)

Tactic:
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
x : ↥(Limits.colimit F)
obtain :
  ∀ (i : (glueData F).J) (xi : ↥((glueData F).U i))
    (h :
      Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
        ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)),
    ∃ (i : J) (xi : ↥(F.obj i)), (colimit.ι F i) xi = x
⊢ ∃ (i : J) (xi : ↥(F.obj i)), (colimit.ι F i) xi = x

Tactic:
obtain ⟨i, xi, h⟩ :=
    (IsLocallyDirected.glueData F).ι_jointly_surjective
      (((IsLocallyDirected.isColimit F).coconePointUniqueUpToIso (colimit.isColimit _)).inv x)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.colimit.isColimit, AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, CategoryTheory.Iso.inv, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
h₁ : (colimit.ι F ↓i) xi = x
⊢ ∃ (i : J) (xi : ↥(F.obj i)), (colimit.ι F i) xi = x

Tactic:
use (equivShrink J).symm i, xi

Premises used: 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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
h₁ :
  Eq (α := ↥(cocone F).pt)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))
        ((colimit.ι F ↓i) xi : ↥(Limits.colimit F)) :
      ↥(cocone F).pt)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
⊢ (colimit.ι F ↓i) xi = x

Tactic:
apply ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv.isOpenEmbedding.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, CategoryTheory.Limits.colimit.isColimit, AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, CategoryTheory.Iso.inv, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
h₁ :
  Eq (α := ↥(cocone F).pt)
    ((CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F ↓i)
          (Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))))
        xi :
      ↥(cocone F).pt)
    (((glueData F).ι i) xi : ↥(glueData F).glued)
⊢ Eq (α := ↥(cocone F).pt)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))
        ((colimit.ι F ↓i) xi : ↥(Limits.colimit F)) :
      ↥(cocone F).pt)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)

Tactic:
simp_rw [← h, colimit.cocone_x, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.colimit.cocone_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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
h₁ :
  CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F ↓i)
      (Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) =
    (glueData F).ι i
⊢ Eq (α := ↥(cocone F).pt)
    ((CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F ↓i)
          (Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))))
        xi :
      ↥(cocone F).pt)
    (((glueData F).ι i) xi : ↥(glueData F).glued)

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
inst_4 : Small.{u, w} J
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
⊢ i = (equivShrink J : (a : J) → Shrink.{u, w} J) (↓i : J)

Tactic:
simp
-- 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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
    ((Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) x : ↥(cocone F).pt)
⊢ (glueData F).ι i ≫ eqToHom ⋯ =
    CategoryStruct.comp (Y := (glueData F).U ((equivShrink J : (a : J) → Shrink.{u, w} J) (↓i : J))) (eqToHom ⋯)
      ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) (↓i : J)))

Tactic:
have := eqToHom_naturality (fun j ↦ (glueData F).ι j)
    (show i = ((equivShrink J) ((equivShrink J).symm i)) by simp)