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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := (glueData F).toLocallyRingedSpaceGlueData.diagram.left (i, j) ⟶ s.pt)
    ((glueData F).toLocallyRingedSpaceGlueData.diagram.fst (i, j) ≫
      (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦
          (s.ι.app ↓i :
            (F ⋙ forgetToLocallyRingedSpace).obj ↓i ⟶
              Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) s.pt) ↓i))
        ((MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).fst (i, j)))
    ((glueData F).toLocallyRingedSpaceGlueData.diagram.snd (i, j) ≫
      (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦
          (s.ι.app ↓i :
            (F ⋙ forgetToLocallyRingedSpace).obj ↓i ⟶
              Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) s.pt) ↓i))
        ((MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).snd (i, j)))

Tactic:
dsimp [glueData, GlueData.diagram]

Premises used: CategoryTheory.GlueData.diagram, AlgebraicGeometry.Scheme.IsLocallyDirected.glueData
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [t, IsOpenImmersion.lift_fac, ← Scheme.Hom.comp_toLRSHom]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.t, AlgebraicGeometry.Scheme.Hom.comp_toLRSHom, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.fromGlued.toLRSHom,
        ← cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.gluedCover.isoLocallyRingedSpace.inv]

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.Scheme.Cover.fromGlued, AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace, AlgebraicGeometry.Scheme.Cover.gluedCover, AlgebraicGeometry.Scheme.Opens.iSupOpenCover, CategoryTheory.cancel_epi, AlgebraicGeometry.Scheme.Cover.ulift, CategoryTheory.Iso.inv
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Multicoequalizer.hom_ext _ _ _ fun ⟨k, hk⟩ ↦ ?_

Premises used: _private.0.AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpace.match_1, AlgebraicGeometry.Scheme.IsLocallyDirected.tAux, AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData, CategoryTheory.GlueData.diagram, AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Cover.fromGlued, CategoryTheory.Limits.Multicoequalizer.hom_ext, CategoryTheory.Limits.colimit, CategoryTheory.Functor.map, Prod.fst, AlgebraicGeometry.Scheme.IsLocallyDirected.V, CategoryTheory.Limits.Cocone.ι, AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Cover.gluedCover, Equiv.symm, AlgebraicGeometry.Scheme.Opens.iSupOpenCover, equivShrink, Sigma.snd, CategoryTheory.Limits.Multicoequalizer.π, AlgebraicGeometry.Scheme.Cover.ulift, Eq, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.GlueData.glued
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
j : J
simp :
  (Hom.toLRSHom (F.map (eqToHom ⋯)) ≫
        ((glueData F).mapGlueData forgetToLocallyRingedSpace).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j) ≫
          Iso.inv (glueData F).isoLocallyRingedSpace) ≫
      Iso.hom (glueData F).isoLocallyRingedSpace ≫
        Multicoequalizer.desc ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram s.pt
          (fun (i : (MultispanShape.prod ((glueData F).mapGlueData forgetToLocallyRingedSpace).J).R) ↦ s.ι.app ↓i) ⋯ =
    s.ι.app j
⊢ (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫
      Iso.hom (glueData F).isoLocallyRingedSpace ≫
        Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
          (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯ =
    s.ι.app j

Tactic:
simp only [cocone, Functor.mapCocone_ι_app, Scheme.Hom.comp_toLRSHom,
      forgetToLocallyRingedSpace_map, ← GlueData.ι_isoLocallyRingedSpace_inv]

Premises used: CategoryTheory.Functor.mapCocone_ι_app, AlgebraicGeometry.Scheme.IsLocallyDirected.cocone, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map, AlgebraicGeometry.Scheme.Hom.comp_toLRSHom, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
j : J
⊢ (Hom.toLRSHom (F.map (eqToHom ⋯)) ≫
        ((glueData F).mapGlueData forgetToLocallyRingedSpace).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j) ≫
          Iso.inv (glueData F).isoLocallyRingedSpace) ≫
      Iso.hom (glueData F).isoLocallyRingedSpace ≫
        Multicoequalizer.desc ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram s.pt
          (fun (i : (MultispanShape.prod ((glueData F).mapGlueData forgetToLocallyRingedSpace).J).R) ↦ s.ι.app ↓i) ⋯ =
    s.ι.app j

Tactic:
simpa [CategoryTheory.GlueData.ι] using s.w _

Premises used: CategoryTheory.GlueData.ι, CategoryTheory.Limits.Cocone.w
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
rw :
  Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
    Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
      (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯
⊢ m =
    Iso.hom (glueData F).isoLocallyRingedSpace ≫
      Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
        (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯

Tactic:
rw [← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
⊢ Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
    Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
      (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯

Tactic:
Multicoequalizer.hom_ext _ _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Multicoequalizer.hom_ext, CategoryTheory.Limits.colimit, CategoryTheory.GlueData.glued
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R),
    Multicoequalizer.π (glueData F).toLocallyRingedSpaceGlueData.diagram i ≫
        Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
      CategoryStruct.comp (Y := multicoequalizer (glueData F).toLocallyRingedSpaceGlueData.diagram)
        (Multicoequalizer.π (glueData F).toLocallyRingedSpaceGlueData.diagram i)
        (Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
          (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯)
⊢ Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
    Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
      (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯

Tactic:
refine Multicoequalizer.hom_ext _ _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Multicoequalizer.hom_ext
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R
dsimp :
  ((glueData F).mapGlueData forgetToLocallyRingedSpace).ι i ≫ Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
    CategoryStruct.comp (Y := multicoequalizer ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram)
      (Multicoequalizer.π ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram i)
      (Multicoequalizer.desc ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram s.pt
        (fun (i : (glueData F).J) ↦ s.ι.app ↓i) ⋯)
⊢ (glueData F).toLocallyRingedSpaceGlueData.ι i ≫ Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
    CategoryStruct.comp (Y := multicoequalizer (glueData F).toLocallyRingedSpaceGlueData.diagram)
      (Multicoequalizer.π (glueData F).toLocallyRingedSpaceGlueData.diagram i)
      (Multicoequalizer.desc (glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
        (fun (i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R) ↦ s.ι.app ↓i) ⋯)

Tactic:
dsimp
-- 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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R
⊢ ((glueData F).mapGlueData forgetToLocallyRingedSpace).ι i ≫ Iso.inv (glueData F).isoLocallyRingedSpace ≫ m =
    CategoryStruct.comp (Y := multicoequalizer ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram)
      (Multicoequalizer.π ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram i)
      (Multicoequalizer.desc ((glueData F).mapGlueData forgetToLocallyRingedSpace).diagram s.pt
        (fun (i : (glueData F).J) ↦ s.ι.app ↓i) ⋯)

Tactic:
simp [cocone, ← hm, glueDataι_naturality,
      ← GlueData.ι_isoLocallyRingedSpace_inv, -ι_gluedIso_inv_assoc, -ι_gluedIso_inv]

Premises used: CategoryTheory.GlueData.ι_gluedIso_inv, AlgebraicGeometry.Scheme.IsLocallyDirected.cocone, CategoryTheory.GlueData.ι_gluedIso_inv_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv
-- 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
⊢ HasColimit F

Tactic:
⟨_, isColimit F⟩

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- 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
⊢ PreservesColimit F forgetToLocallyRingedSpace

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimit F) (isColimitForgetToLocallyRingedSpace F)

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit, AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpace, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- 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
⊢ IsOpenImmersion (Y := Limits.colimit F) (colimit.ι F i)

Tactic:
inferInstanceAs (IsOpenImmersion ((openCover F).f i))

Premises used: _private.0.AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι._proof_1
-- 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 : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
mp :
  Eq (α := ↥(Limits.colimit F)) ((colimit.ι F i) xi : ↥(Limits.colimit F)) ((colimit.ι F j) xj : ↥(Limits.colimit F)) →
    ∃ (k : J) (fi : k ⟶ i) (fj : k ⟶ j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj
mpr :
  (∃ (k : J) (fi : k ⟶ i) (fj : k ⟶ j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj) →
    Eq (α := ↥(Limits.colimit F)) ((colimit.ι F i) xi : ↥(Limits.colimit F)) ((colimit.ι F j) xj : ↥(Limits.colimit F))
⊢ Eq (α := ↥(Limits.colimit F)) ((colimit.ι F i) xi : ↥(Limits.colimit F)) ((colimit.ι F j) xj : ↥(Limits.colimit F)) ↔
    ∃ (k : J) (fi : k ⟶ i) (fj : k ⟶ j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i j k : J
fi : k ⟶ i
fj : k ⟶ j
x : ↥(F.obj k)
⊢ Eq (α := ↥(Limits.colimit F)) ((colimit.ι F i) ((F.map fi) x : ↥(F.obj i)) : ↥(Limits.colimit F))
    ((colimit.ι F j) ((F.map fj) x : ↥(F.obj j)) : ↥(Limits.colimit F))

Tactic:
simp only [← Scheme.Hom.comp_apply, colimit.w]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.colimit.w
-- 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 : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
mp :
  ∀ (i : Shrink.{u, w} J) {xi : ↥(F.obj ↓i)},
    Eq (α := ↥(Limits.colimit F)) ((colimit.ι F ↓i) xi : ↥(Limits.colimit F))
        ((colimit.ι F j) xj : ↥(Limits.colimit F)) →
      ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj
⊢ Eq (α := ↥(Limits.colimit F)) ((colimit.ι F i) xi : ↥(Limits.colimit F)) ((colimit.ι F j) xj : ↥(Limits.colimit F)) →
    ∃ (k : J) (fi : k ⟶ i) (fj : k ⟶ j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

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

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
j : J
xj : ↥(F.obj j)
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
mp :
  ∀ (j : Shrink.{u, w} J) {xj : ↥(F.obj ↓j)},
    Eq (α := ↥(Limits.colimit F)) ((colimit.ι F ↓i) xi : ↥(Limits.colimit F))
        ((colimit.ι F ↓j) xj : ↥(Limits.colimit F)) →
      ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj
⊢ Eq (α := ↥(Limits.colimit F)) ((colimit.ι F ↓i) xi : ↥(Limits.colimit F)) ((colimit.ι F j) xj : ↥(Limits.colimit F)) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

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

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 : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
mp :
  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)))
          ((colimit.ι F ↓j) xj : ↥(Limits.colimit F)) :
        ↥(cocone F).pt) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj
⊢ Eq (α := ↥(Limits.colimit F)) ((colimit.ι F ↓i) xi : ↥(Limits.colimit F))
      ((colimit.ι F ↓j) xj : ↥(Limits.colimit F)) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
rw [← ((isColimit F).coconePointUniqueUpToIso
    (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Function.Injective.eq_iff, 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
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
mp :
  Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
      (((glueData F).ι j) xj : ↥(glueData F).glued) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj
⊢ 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)))
          ((colimit.ι F ↓j) xj : ↥(Limits.colimit F)) :
        ↥(cocone F).pt) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
simp only [Limits.colimit, ← Scheme.Hom.comp_apply,
    colimit.comp_coconePointUniqueUpToIso_inv, cocone, glueDataι_naturality]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.cocone, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.colimit, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
-- 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)
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
      (((glueData F).ι j) xj : ↥(glueData F).glued) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
?_ ∘ ((glueData F).ι_eq_iff _ _ _ _).mp

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, Function.comp, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, Iff.mp
-- 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 :
  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
⊢ Eq (α := ↥(glueData F).glued) (((glueData F).ι i) xi : ↥(glueData F).glued)
      (((glueData F).ι j) xj : ↥(glueData F).glued) →
    ∃ (k : J) (fi : k ⟶ ↓i) (fj : k ⟶ ↓j) (x : ↥(F.obj k)), (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
refine ?_ ∘ ((glueData F).ι_eq_iff _ _ _ _).mp

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, Iff.mp