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
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))
⊢ 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))
have 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))
Tactic: obtain ⟨k, rfl⟩ := (equivShrink J).symm.surjective k
Cleared hypotheses: k, ki, kj, y, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
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 (α := ↥(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))
have 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)
Tactic: apply ((glueData F).ι _).isOpenEmbedding.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
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)
    (((glueData F).ι j) (((glueData F).t i j ≫ (glueData F).f j i) x : ↥((glueData F).U j)) : ↥(glueData F).glued)
have 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)
Tactic: simp only [← Scheme.Hom.comp_apply, Category.assoc, GlueData.glue_condition]
-- 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 : 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)
    (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)
have 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)
Tactic: trans (glueData F).ι k y
-- 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 : 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)
⊢ 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)
have trans₁ : Eq (α := ↥(glueData F).glued) (((glueData F).ι k) y : ↥(glueData F).glued)
  (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)
Tactic: trans (glueData F).ι k y
-- 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 : 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)
    (((glueData F).ι k) y : ↥(glueData F).glued)
have 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)
Tactic: simp [← glueDataι_naturality F kj]
-- 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 : 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).ι k) y : ↥(glueData F).glued)
    (((glueData F).f i j ≫ (glueData F).ι i) x : ↥(glueData F).glued)
have 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)
Tactic: simp [← glueDataι_naturality F ki, ← hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
x : ↥(Limits.colimit F)
⊢ ∃ (i : J) (xi : ↥(F.obj i)), (colimit.ι F i) xi = x
have 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
Tactic: obtain ⟨i, xi, h⟩ :=
    (IsLocallyDirected.glueData F).ι_jointly_surjective
      (((IsLocallyDirected.isColimit F).coconePointUniqueUpToIso (colimit.isColimit _)).inv x)
-- 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
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 : J) (xi : ↥(F.obj i)), (colimit.ι F i) xi = x
have h₁ : (colimit.ι F ↓i) xi = x
Tactic: use (equivShrink J).symm 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
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)
⊢ (colimit.ι F ↓i) xi = x
have 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)
Tactic: apply ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv.isOpenEmbedding.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
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)
⊢ 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)
have 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)
Tactic: simp_rw [← h, colimit.cocone_x, ← Scheme.Hom.comp_apply]
-- 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
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)
⊢ 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)
have h₁ : CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F ↓i)
    (Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) =
  (glueData F).ι i
Tactic: congr 5
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
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)
⊢ CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F ↓i)
      (Iso.inv (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))) =
    (glueData F).ι i
have this : (glueData F).ι i ≫ eqToHom sorry =
  CategoryStruct.comp (Y := (glueData F).U ((equivShrink J : (a : J) → Shrink.{u, w} J) (↓i : J))) (eqToHom sorry)
    ((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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GluingOneHypercover (goal)
Goal:
D : GlueData
⊢ Membership.mem (γ := Set (Sieve D.glued)) ((zariskiTopology : (a : Scheme) → Set (Sieve a)) D.glued)
    { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.sieve₀
have refine : Sieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀
Tactic: refine zariskiTopology.superset_covering ?_ D.openCover.mem_grothendieckTopology
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GluingOneHypercover (goal)
Goal:
D : GlueData
⊢ Sieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀
have rw : Presieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀.arrows
Tactic: rw [Sieve.generate_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GluingOneHypercover (goal)
Goal:
D : GlueData
Y : Scheme
i : D.openCover.I₀
⊢ 𝟙 (D.openCover.X i) ≫ { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i = D.openCover.f i
have simp : D.ι i = D.openCover.f i
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GluingOneHypercover (goal)
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
⊢ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
          Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
          p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
          p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
          PreOneHypercover D.glued }.sieve₁
      p₁ p₂ ∈
    (zariskiTopology : (a : Scheme) → Set (Sieve a)) W
have refine : ∀ (T : Scheme.{u}) (g : T ⟶ W),
  Sieve.arrows ⊤ g →
    ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
              Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
              p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
              p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := sorry :
              PreOneHypercover D.glued }.sieve₁
          p₁ p₂).arrows
      g
Tactic: refine zariskiTopology.superset_covering (fun T g _ ↦ ?_) (zariskiTopology.top_mem _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GluingOneHypercover (goal)
Goal:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
h : Sieve.arrows ⊤ g
⊢ ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
            Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
            p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
            p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ :
            PreOneHypercover D.glued }.sieve₁
        p₁ p₂).arrows
    g
have have : ∀ (φ : T ⟶ (D.vPullbackCone i₁ i₂).pt) (h₁ : φ ≫ (D.vPullbackCone i₁ i₂).fst = g ≫ p₁)
  (h₂ : φ ≫ (D.vPullbackCone i₁ i₂).snd = g ≫ p₂),
  ({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun (x x_1 : D.J) ↦ PUnit.{u + 1},
            Y := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.V (i₁, i₂),
            p₁ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.f i₁ i₂,
            p₂ := fun (i₁ i₂ : D.J) (x : PUnit.{u + 1}) ↦ D.t i₁ i₂ ≫ D.f i₂ i₁, w := sorry :
            PreOneHypercover D.glued }.sieve₁
        p₁ p₂).arrows
    g
Tactic: have ⟨φ, h₁, h₂⟩ := PullbackCone.IsLimit.lift' (D.vPullbackConeIsLimit i₁ i₂)
      (g ≫ p₁) (g ≫ p₂) (by simpa using g ≫= fac)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
⊢ IsCommMonObj G
have hpoint : IsClosed (X := ↥S) {point}
Tactic: have hpoint : IsClosed {point} := isClosed_discrete _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
⊢ IsCommMonObj G
have this : Nonempty.{u + 1} ↥G.left
Tactic: have : Nonempty G.left := ⟨η[G].left point⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (goal)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this : Nonempty.{u + 1} ↥G.left
⊢ IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
have dsimp : IsProper (X := pullback G.hom G.hom) (pullback.fst G.hom G.hom ≫ G.hom)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this : Nonempty.{u + 1} ↥G.left
⊢ IsCommMonObj G
have this₁ : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
Tactic: have : IsProper (G ⊗ G).hom := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
⊢ IsCommMonObj G
have this₁ : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
Tactic: have : JacobsonSpace (G ⊗ G).left := LocallyOfFiniteType.jacobsonSpace (Y := Spec _) (G ⊗ G).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
⊢ IsCommMonObj G
have this₁ : Surjective G.hom
Tactic: have : Surjective G.hom := ⟨Function.surjective_to_subsingleton (α := G.left) (β := Spec _) _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this : Surjective G.hom
⊢ IsCommMonObj G
have this₁ : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
Tactic: have : IsProper (fst G G).left := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Abelian (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst_2 : IsProper G.hom
inst_3 : IsIntegral.{u} (tensorObj (𝒞 := instCategoryOver) G G).left
inst_4 : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed (X := ↥S) {point}
this_1 : Nonempty.{u + 1} ↥G.left
this_2 : IsProper (tensorObj (𝒞 := instCategoryOver) G G).hom
this_3 : JacobsonSpace.{u} ↥(tensorObj (𝒞 := instCategoryOver) G G).left
this_4 : Surjective G.hom
this : IsProper (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
⊢ IsCommMonObj G
have this₁ : Surjective (X := (tensorObj (𝒞 := instCategoryOver) G G).left) (Over.Hom.left (fst G G))
Tactic: have : Surjective (fst G G).left := by dsimp; infer_instance