awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_4 : Small.{u, w} J
s : Cocone F
j : J
⊢ (cocone F).ι.app j ≫
      Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯ =
    s.ι.app j
have refine : F.map (eqToHom sorry) ≫
    CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
      ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
      (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        sorry) =
  s.ι.app j
Tactic: refine (Category.assoc _ _ _).trans ?_
-- 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
inst_4 : Small.{u, w} J
s : Cocone F
j : J
| (F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) :
    F.obj j ⟶ s.pt)
have enter : CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
  ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
  (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i) sorry)
Tactic: enter [2]
-- 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
inst_4 : Small.{u, w} J
s : Cocone F
j : J
| (F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) :
    F.obj j ⟶ s.pt)
have enter : CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
  ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
  (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i) sorry)
Tactic: enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _
-- 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
inst_4 : Small.{u, w} J
s : Cocone F
j : J
⊢ F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) =
    s.ι.app j
have conv_lhs : CategoryStruct.comp (Y := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J)) (F.map (eqToHom sorry))
    (s.ι.app ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J)) =
  s.ι.app j
Tactic: conv_lhs => enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _
-- 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
inst_4 : Small.{u, w} J
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : J), (cocone F).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).J).R
⊢ Multicoequalizer.π (glueData F).diagram i ≫ m =
    CategoryStruct.comp (Y := multicoequalizer (glueData F).diagram) (Multicoequalizer.π (glueData F).diagram i)
      (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯)
have simp : Multicoequalizer.π (glueData F).diagram i ≫ m = (glueData F).ι i ≫ m
Tactic: simp [← hm ↓i, cocone, reassoc_of% glueDataι_naturality]
-- 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
inst_4 : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ 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)))
have dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp [glueData, GlueData.diagram]
-- 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
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)
have simp : 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]
-- 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
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)
have rw : 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]
-- 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
inst_4 : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
j : 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
have simp : (Hom.toLRSHom (F.map (eqToHom sorry)) ≫
      ((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) sorry =
  s.ι.app j
Tactic: simp only [cocone, Functor.mapCocone_ι_app, Scheme.Hom.comp_toLRSHom,
      forgetToLocallyRingedSpace_map, ← GlueData.ι_isoLocallyRingedSpace_inv]
-- 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
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
⊢ 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) ⋯
have 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) sorry
Tactic: rw [← Iso.inv_comp_eq]
-- 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
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) ⋯
have 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) sorry)
Tactic: refine Multicoequalizer.hom_ext _ _ _ fun i ↦ ?_
-- 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
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).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) ⋯)
have 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) sorry)
Tactic: dsimp
-- 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
inst_4 : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
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
have 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
Tactic: constructor
-- 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
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
⊢ 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
have 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))
Tactic: constructor
-- 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
inst_4 : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
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
have 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
Tactic: obtain ⟨i, rfl⟩ := (equivShrink J).symm.surjective i
Cleared hypotheses: i, xi
-- 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
inst_4 : Small.{u, w} J
j : J
xj : ↥(F.obj j)
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
have 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
Tactic: obtain ⟨j, rfl⟩ := (equivShrink J).symm.surjective j
Cleared hypotheses: j, xj
-- 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
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 (α := ↥(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
have 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
Tactic: rw [← ((isColimit F).coconePointUniqueUpToIso
    (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff]
-- 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
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 (α := ↥(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
have 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
Tactic: simp only [Limits.colimit, ← Scheme.Hom.comp_apply,
    colimit.comp_coconePointUniqueUpToIso_inv, cocone, glueDataι_naturality]
-- 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
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
have 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
Tactic: refine ?_ ∘ ((glueData F).ι_eq_iff _ _ _ _).mp
-- 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
inst_4 : Small.{u, w} J
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ 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
have 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
Tactic: dsimp +instances only [GlueData.Rel]
-- 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
inst_4 : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, 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))
have 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))
Tactic: obtain ⟨⟨k, ki, kj⟩, y, hy : F.map ki y = (glueData F).f i j x⟩ := mem_iSup.mp x.2
-- 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
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))
have 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))
Tactic: refine ⟨k, ki, kj, y, hy, ?_⟩