awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
x : ↥(image f)
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
⊢ Function.Injective (α :=
    (↑((image f).presheaf.obj (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) : Type u))
    (β :=
    (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toImage f).base) X.presheaf).obj
          (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X :=
          (image f).presheaf.obj (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ }))
          ((toImage f).c.app (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ }))) :
      (a :
          (↑((image f).presheaf.obj (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) :
            Type u)) →
        (↑(((TopCat.Presheaf.pushforward CommRingCat (toImage f).base).obj X.presheaf).obj
              (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) :
          Type u))

Tactic:
exact f.toImage_app_injective ⟨U, hU⟩

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_app_injective, Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
I : Y.IdealSheafData
⊢ Functor.obj (𝟭 Y.IdealSheafData) I = ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor).obj I

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
x x_1 : (Over Y)ᵒᵖ
x_2 : x ⟶ x_1
h :
  Eq (α :=
    (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
      (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
    (Over.Hom.left
        (Quiver.Hom.unop
          ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x_2 ≫
            Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x_1).hom) ⋯))) :
      (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
        (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
    (Over.Hom.left
        (Quiver.Hom.unop
          (Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x).hom) ⋯) ≫
            CategoryTheory.Functor.map (𝟭 (Over Y)ᵒᵖ) x_2)) :
      (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
        (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
⊢ Eq (α :=
    Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1) ⟶
      Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x))
    (Quiver.Hom.unop
        ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x_2 ≫
          Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x_1).hom) ⋯)) :
      Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1) ⟶
        Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x))
    (Quiver.Hom.unop
        (Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x).hom) ⋯) ≫
          CategoryTheory.Functor.map (𝟭 (Over Y)ᵒᵖ) x_2) :
      Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1) ⟶
        Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x))

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
x x_1 : (Over Y)ᵒᵖ
x_2 : x ⟶ x_1
⊢ Eq (α :=
    (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
      (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
    (Over.Hom.left
        (Quiver.Hom.unop
          ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x_2 ≫
            Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x_1).hom) ⋯))) :
      (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
        (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)
    (Over.Hom.left
        (Quiver.Hom.unop
          (Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop x).hom) ⋯) ≫
            CategoryTheory.Functor.map (𝟭 (Over Y)ᵒᵖ) x_2)) :
      (Opposite.unop (Functor.obj (𝟭 (Over Y)ᵒᵖ) x_1)).left ⟶
        (Opposite.unop ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).obj x)).left)

Tactic:
simp [← cancel_mono (subschemeι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
I : Y.IdealSheafData
h :
  Over.Hom.left
      (Quiver.Hom.unop
        ((subschemeFunctor Y).rightOp.map
            ({ app := fun (I : Y.IdealSheafData) ↦ eqToHom ⋯, naturality := ⋯ :
                  NatTrans (𝟭 Y.IdealSheafData) ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor) }.app
              I) ≫
          NatTrans.app
            { app := fun (f : (Over Y)ᵒᵖ) ↦ Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯),
              naturality := ⋯ }
            ((subschemeFunctor Y).rightOp.obj I))) =
    Over.Hom.left (Quiver.Hom.unop (𝟙 ((subschemeFunctor Y).rightOp.obj I)))
⊢ Quiver.Hom.unop
      ((subschemeFunctor Y).rightOp.map
          ({ app := fun (I : Y.IdealSheafData) ↦ eqToHom ⋯, naturality := ⋯ :
                NatTrans (𝟭 Y.IdealSheafData) ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor) }.app
            I) ≫
        NatTrans.app
          { app := fun (f : (Over Y)ᵒᵖ) ↦ Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯),
            naturality := ⋯ }
          ((subschemeFunctor Y).rightOp.obj I)) =
    Quiver.Hom.unop (𝟙 ((subschemeFunctor Y).rightOp.obj I))

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y_1 : Scheme
f : X ⟶ Y_1
U : (↑Y_1.affineOpens : Type u)
Y : Scheme
I : Y.IdealSheafData
⊢ Over.Hom.left
      (Quiver.Hom.unop
        ((subschemeFunctor Y).rightOp.map
            ({ app := fun (I : Y.IdealSheafData) ↦ eqToHom ⋯, naturality := ⋯ :
                  NatTrans (𝟭 Y.IdealSheafData) ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor) }.app
              I) ≫
          NatTrans.app
            { app := fun (f : (Over Y)ᵒᵖ) ↦ Quiver.Hom.op (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯),
              naturality := ⋯ }
            ((subschemeFunctor Y).rightOp.obj I))) =
    Over.Hom.left (Quiver.Hom.unop (𝟙 ((subschemeFunctor Y).rightOp.obj I)))

Tactic:
simp [← cancel_mono (subschemeι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
⊢ IsIso Y.kerAdjunction.rightOp.counit

Tactic:
simp [NatTrans.isIso_iff_isIso_app, CategoryTheory.instIsIsoEqToHom]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.instIsIsoEqToHom
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ HasTerminal Scheme

Tactic:
hasTerminal_of_hasTerminal_of_preservesLimit Scheme.Spec

Premises used: CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit, AlgebraicGeometry.Scheme.Spec
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ IsAffine.{u} (⊤_ Scheme)

Tactic:
.of_isIso (PreservesTerminal.iso Scheme.Spec).inv

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Limits.PreservesTerminal.iso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ HasFiniteLimits Scheme

Tactic:
hasFiniteLimits_of_hasTerminal_and_pullbacks

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
inst : X.Over (⊤_ Scheme)
inst_1 : Y.Over (⊤_ Scheme)
f : X ⟶ Y
⊢ Scheme.Hom.IsOver f (⊤_ Scheme)

Tactic:
⟨Subsingleton.elim _ _⟩

Premises used: CategoryTheory.HomIsOver.mk, Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
x x_1 : X.Over (⊤_ Scheme)
a b : X ⟶ ⊤_ Scheme
⊢ { hom := a : OverClass X (⊤_ Scheme) } = { hom := b }

Tactic:
simp [Subsingleton.elim a b]

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
⊢ Continuous (Y := (↑X.toPresheafedSpace.1 : Type u)) fun (x : PEmpty.{u + 1}) ↦ x.elim

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
f g : ∅ ⟶ X
⊢ f = g

Tactic:
Scheme.Hom.ext' (Subsingleton.elim (α := ∅ ⟶ _) _ _)

Premises used: AlgebraicGeometry.Scheme.Hom.ext', Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
f : ∅ ⟶ X
⊢ f = X.emptyTo

Tactic:
Scheme.empty_ext f (Scheme.emptyTo X)

Premises used: AlgebraicGeometry.Scheme.empty_ext, AlgebraicGeometry.Scheme.emptyTo
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ emptyIsInitial.to = Scheme.emptyTo

Tactic:
rfl

Premises used: Set.Mem, CategoryTheory.Limits.IsInitial.to, AlgebraicGeometry.Scheme.emptyTo, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ IsEmpty PEmpty.{u + 1}

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ IsEmpty.{u + 1} ↥(Spec (CommRingCat.of PUnit.{u + 1}))

Tactic:
inferInstanceAs <| IsEmpty (PrimeSpectrum PUnit)

Premises used: _private.0.AlgebraicGeometry.spec_punit_isEmpty._proof_1
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : IsEmpty.{u_1 + 1} ↥X
hf : Topology.IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
inst : ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
⊢ IsOpenImmersion f

Tactic:
apply +allowSynthFailures IsOpenImmersion.of_isIso_stalkMap

Premises used: AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥X
⊢ Topology.IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
.of_isEmpty (X := X) _

Premises used: Topology.IsOpenEmbedding.of_isEmpty
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥X
⊢ Topology.IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
exact .of_isEmpty (X := X) _
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥X
i : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f i)

Tactic:
isEmptyElim i

Premises used: isEmptyElim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥X
i : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f i)

Tactic:
exact isEmptyElim i
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
⊢ IsEmpty.{u_1 + 1} ↥X

Tactic:
haveI : IsEmpty X := f.base.hom.1.isEmpty
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this : IsEmpty.{u_1 + 1} ↥X
rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
⊢ Epi f.base

Tactic:
rw [TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this : IsEmpty.{u_1 + 1} ↥X
x : ↥Y
⊢ ∃ (a : ↥X), f a = x

Tactic:
isEmptyElim x

Premises used: isEmptyElim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this : IsEmpty.{u_1 + 1} ↥X
x : ↥Y
⊢ ∃ (a : ↥X), f a = x

Tactic:
exact isEmptyElim x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this : IsEmpty.{u_1 + 1} ↥X
⊢ Epi f.base

Tactic:
have : Epi f.base := by
    rw [TopCat.epi_iff_surjective]; rintro (x : Y)
    exact isEmptyElim x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsEmpty.{u_1 + 1} ↥Y
this_1 : IsEmpty.{u_1 + 1} ↥X
this : Epi f.base
⊢ IsIso f

Tactic:
apply IsOpenImmersion.isIso

Premises used: AlgebraicGeometry.IsOpenImmersion.isIso
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
⊢ Nonempty.{u + 2} (IsInitial X) ↔ IsEmpty.{u + 1} ↥X

Tactic:
⟨fun ⟨h⟩ ↦ (h.uniqueUpToIso specPUnitIsInitial).hom.homeomorph.isEmpty,
    fun _ ↦ ⟨isInitialOfIsEmpty⟩⟩

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.isInitialOfIsEmpty, CategoryTheory.Limits.IsInitial.uniqueUpToIso, Homeomorph.toEquiv, IsEmpty, Nonempty.intro, Equiv.isEmpty, AlgebraicGeometry.Scheme.Hom.homeomorph, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, _private.0.AlgebraicGeometry.isInitial_iff_isEmpty.match_1, TopCat.carrier, AlgebraicGeometry.specPUnitIsInitial, Iff.intro, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : IsEmpty.{u_1 + 1} ↥X
⊢ IsAffine X

Tactic:
.of_isIso (inv (emptyIsInitial.to X) ≫ emptyIsInitial.to (Spec <| .of PUnit))

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.Limits.IsInitial.to, AlgebraicGeometry.emptyIsInitial, PUnit, CommRingCat.of, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ HasInitial Scheme

Tactic:
hasInitial_of_unique ∅

Premises used: CategoryTheory.Limits.hasInitial_of_unique, EmptyCollection.emptyCollection
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
⊢ IsEmpty.{u_1 + 1} ↥(⊥_ Scheme)

Tactic:
⟨fun x => ((initial.to Scheme.empty :) x).elim⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.initial.to, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', PEmpty.elim, IsEmpty.mk, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.empty, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
⊢ IsAffineOpen.{u_1} (X := X) ⊥

Tactic:
@isAffine_of_isEmpty _ (inferInstanceAs (IsEmpty (∅ : Set X)))

Premises used: AlgebraicGeometry.isAffine_of_isEmpty, AlgebraicGeometry.IsAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
A : Scheme
f : A ⟶ ⊥_ Scheme
⊢ IsIso f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : IsEmpty.{u_1 + 1} ↥X
U : X.Opens
⊢ U = ⊥

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : IsEmpty.{u_1 + 1} ↥X
U : X.Opens
obtain : Subsingleton.{u_1 + 1} (↑Γ(X, ⊥) : Type u_1)
⊢ Subsingleton.{u_1 + 1} (↑Γ(X, U) : Type u_1)

Tactic:
obtain rfl : U = ⊥ := Subsingleton.elim _ _

Premises used: Subsingleton.elim, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : IsEmpty.{u_1 + 1} ↥X
⊢ Subsingleton.{u_1 + 1} (↑Γ(X, ⊥) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
h : IsEmpty.{u + 1} ↥X
⊢ IsAffine X

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
h : Nonempty.{u + 1} ↥X
inr : ∀ (x : ↥X), IsAffine X
⊢ IsAffine X

Tactic:
obtain ⟨x⟩ := h
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
⊢ Membership.mem (γ := Set ↥X) Set.univ x

Tactic:
trivial
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
inr : ∀ (U : Opens ↥X) (hU : IsAffine.{u} (↑U : Scheme)) (hxU : x ∈ (↑U : Set ↥X)), IsAffine X
⊢ IsAffine X

Tactic:
obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ

Premises used: AlgebraicGeometry.IsAffine, isOpen_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
h : ∀ (y : ↥X), y ∈ (↑U : Set ↥X) ↔ y ∈ (↑⊤ : Set ↥X)
⊢ U = ⊤

Tactic:
ext y
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
y : ↥X
⊢ y ∈ (↑U : Set ↥X) ↔ y ∈ (↑⊤ : Set ↥X)

Tactic:
simpa [Subsingleton.elim y x]

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
⊢ IsAffine.{u} (↑⊤ : Scheme)

Tactic:
obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine.{u} (↑U : Scheme)
hxU : x ∈ (↑U : Set ↥X)
hU₁ : IsAffine.{u} (↑⊤ : Scheme)
⊢ x ∈ (↑⊤ : Set ↥X)

Tactic:
obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
hU : IsAffine.{u} (↑⊤ : Scheme)
hxU : x ∈ (↑⊤ : Set ↥X)
⊢ IsAffine X

Tactic:
.of_isIso (Scheme.topIso X).inv

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.Scheme.topIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
x : ↥X
hU : IsAffine.{u} (↑⊤ : Scheme)
hxU : x ∈ (↑⊤ : Set ↥X)
⊢ IsAffine X

Tactic:
exact .of_isIso (Scheme.topIso X).inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
⊢ IsEmpty.{u + 1} ↥X ∨ Nonempty.{u + 1} ↥X

Tactic:
cases isEmpty_or_nonempty X with
  | inl h => infer_instance
  | inr h =>
  obtain ⟨x⟩ := h
  obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ
  obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]
  exact .of_isIso (Scheme.topIso X).inv

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, isEmpty_or_nonempty, AlgebraicGeometry.IsAffine, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, rfl, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
U : X.Opens
hU : (↑U : Set ↥X).Subsingleton
⊢ IsAffineOpen U

Tactic:
have : Subsingleton U := hU.coe_sort
  inferInstanceAs (IsAffine _)

Premises used: AlgebraicGeometry.instIsAffineOfSubsingletonCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen, Set.Subsingleton.coe_sort
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
⊢ PreservesColimitsOfShape.{v, v, u, u, u + 1, u + 1} (Discrete σ) Scheme.forgetToTop

Tactic:
inferInstanceAs (PreservesColimitsOfShape (Discrete σ) (Scheme.forgetToLocallyRingedSpace ⋙
      LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat))

Premises used: _private.0.AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall._proof_1
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete σ) Scheme

Tactic:
⟨fun _ ↦ hasColimit_of_created _ Scheme.forgetToLocallyRingedSpace⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.hasColimit_of_created
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ↔
    Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)

Tactic:
(Scheme.IsLocallyDirected.ι_eq_ι_iff _).trans ⟨?_, ?_⟩

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, Iff.intro, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
refine_1 :
  (∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y) →
    Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)
refine_2 :
  Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y) →
    ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ↔
    Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y)

Tactic:
refine (Scheme.IsLocallyDirected.ι_eq_ι_iff _).trans ⟨?_, ?_⟩

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, Iff.intro, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
k : Discrete σ
x : ↥(Functor.obj (Discrete.functor g) k)
⊢ Eq (α := (i : σ) × ↥(g i))
    (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) k.1
        ((CategoryTheory.Functor.map (Discrete.functor g) { down := { down := ⋯ } }) x) :
      (i : σ) × ↥(g i))
    (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) k.1
        ((CategoryTheory.Functor.map (Discrete.functor g) { down := { down := ⋯ } }) x) :
      (i : σ) × ↥(g i))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
refine_2 :
  i = j ∧ x ≍ y →
    ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(g k.as)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y
⊢ Eq (α := (i : σ) × ↥(g i)) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) i x) (Sigma.mk (β := fun (i : σ) ↦ ↥(g i)) j y) →
    ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := j }) (x_1 : ↥(Functor.obj (Discrete.functor g) k)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y

Tactic:
simp only [Discrete.functor_obj_eq_as, Sigma.mk.injEq]

Premises used: Sigma.mk.injEq, CategoryTheory.Discrete.functor_obj_eq_as
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i : σ
x y : ↥(g i)
e : x ≍ y
refine_2 :
  ∀ (e : x ≍ x),
    ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := i }) (x_1 : ↥(g k.as)),
      (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
        (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = x
⊢ ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := i }) (x_1 : ↥(g k.as)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = y

Tactic:
obtain rfl := (heq_eq_eq x y).mp e

Premises used: heq_eq_eq, Eq.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i : σ
x : ↥(g i)
e : x ≍ x
⊢ (CategoryTheory.Functor.map (Discrete.functor g) (𝟙 { as := i })) x = x ∧
    (CategoryTheory.Functor.map (Discrete.functor g) (𝟙 { as := i })) x = x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i : σ
x : ↥(g i)
e : x ≍ x
⊢ ∃ (k : Discrete σ) (fi : k ⟶ { as := i }) (fj : k ⟶ { as := i }) (x_1 : ↥(g k.as)),
    (CategoryTheory.Functor.map (Discrete.functor g) fi) x_1 = x ∧
      (CategoryTheory.Functor.map (Discrete.functor g) fj) x_1 = x

Tactic:
exact ⟨⟨i⟩, 𝟙 _, 𝟙 _, x, by simp⟩
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(∐ g)
hx : x ∈ U
obtain :
  ∀ (x : ↥(g i)) (hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))),
    Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
⊢ Membership.mem (γ := Opens ↥(∐ g)) ⊥ x

Tactic:
obtain ⟨x, rfl⟩ := hU hx

Premises used: rfl