awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
g : (↑Γ(Y, ⊤) : Type u)
h :
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro) :
          (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
            g :
          (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
U : Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
w : U ⟶ ⊤
hx : x ∈ U
hg :
  Eq (α := (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toRingedSpace.presheaf.map w.op) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) → (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) φ :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            g :
          (↑Γ(X, ⊤) : Type u)) :
      (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    (0 : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
⊢ x ∈ U.carrier ∧ Eq (α := ↥Y) (f x : ↥Y) (f x : ↥Y)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
g : (↑Γ(Y, ⊤) : Type u)
h :
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro) :
          (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
            g :
          (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
U : Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
w : U ⟶ ⊤
hx : x ∈ U
hg :
  Eq (α := (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toRingedSpace.presheaf.map w.op) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) → (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) φ :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            g :
          (↑Γ(X, ⊤) : Type u)) :
      (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    (0 : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
s : (↑Γ(Y, ⊤) : Type u)
hyv : Membership.mem (α := ↥Y) (Y.basicOpen s) (f x : ↥Y)
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun (i : 𝒰.I₀) ↦
    (𝒰.X i).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (res i) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(𝒰.X i, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          s))
i : 𝒰.I₀
⊢ f ⁻¹ᵁ { carrier := ⇑f '' U.carrier, is_open' := ⋯ : Opens ↥Y } = U

Tactic:
simp [Set.preimage_image_eq _ hfinj₁]

Premises used: Set.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
g : (↑Γ(Y, ⊤) : Type u)
h :
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro) :
          (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
            g :
          (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
U : Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
w : U ⟶ ⊤
hx : x ∈ U
hg :
  Eq (α := (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.toRingedSpace.presheaf.map w.op) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op ⊤)) : Type u)) → (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) φ :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            g :
          (↑Γ(X, ⊤) : Type u)) :
      (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
    (0 : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u))
s : (↑Γ(Y, ⊤) : Type u)
hyv : Membership.mem (α := ↥Y) (Y.basicOpen s) (f x : ↥Y)
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun (i : 𝒰.I₀) ↦
    (𝒰.X i).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (res i) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(𝒰.X i, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ W i ≤ 𝒰.f i ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
hf :
  Function.Injective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
⊢ (Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) =
    Scheme.IdealSheafData.ideal ⊥ (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)

Tactic:
simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot]

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Scheme.Hom.ker_apply, Subtype.mk, RingHom.injective_iff_ker_eq_bot, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
⊢ IsAffine X ∧
    Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f)) :
        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
⟨isAffine_of_isAffineHom f, ?_⟩

Premises used: AlgebraicGeometry.isAffine_of_isAffineHom, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
refine :
  Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
⊢ IsAffine X ∧
    Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f)) :
        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
refine ⟨isAffine_of_isAffineHom f, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
simp :
  Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (Function.comp (β := (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.toImage f))) :
        (a : (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.ker f).subschemeι)) :
        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)))
⊢ Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
simp only [← f.toImage_imageι, Scheme.Hom.comp_appTop, CommRingCat.hom_comp, RingHom.coe_comp,
    Scheme.Hom.image, Scheme.Hom.imageι]

Premises used: AlgebraicGeometry.Scheme.Hom.image, AlgebraicGeometry.Scheme.Hom.imageι, AlgebraicGeometry.Scheme.Hom.toImage_imageι, CommRingCat.hom_comp, RingHom.coe_comp, AlgebraicGeometry.Scheme.Hom.comp_appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
rw :
  Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (Function.comp (β := (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.toImage f) ⊤)) :
        (a : (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
      (Function.comp (β :=
        (↑(CommRingCat.of
              (HasQuotient.Quotient
                (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u) (B :=
                Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u))
                ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
          Type u))
        (⇑(CommRingCat.Hom.hom
              (Iso.inv
                ((Scheme.Hom.ker f).subschemeObjIso (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
          (a : (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, ⋯⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩)) : Type u)) →
            (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
        (⇑(CommRingCat.Hom.hom
                (CommRingCat.ofHom
                  (Ideal.Quotient.mk
                    ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
              (↑Γ(Y, ⊤) : Type u) →+*
                (↑(CommRingCat.of
                      (HasQuotient.Quotient
                        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u)
                        (B :=
                        Ideal
                          (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u))
                        ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
                  Type u)) :
          (a : (↑Γ(Y, ⊤) : Type u)) →
            (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, ⋯⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩)) : Type u))))
⊢ Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (Function.comp (β := (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.toImage f))) :
        (a : (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.ker f).subschemeι)) :
        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)))

Tactic:
rw [Scheme.Hom.appTop, Scheme.Hom.appTop, f.ker.subschemeι_app ⟨⊤, isAffineOpen_top Y⟩,
    CommRingCat.hom_comp, RingHom.coe_comp]

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.Scheme.Hom.ker, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, Subtype.mk, RingHom.coe_comp, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
⊢ Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (Function.comp (β := (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.toImage f) ⊤)) :
        (a : (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
      (Function.comp (β :=
        (↑(CommRingCat.of
              (HasQuotient.Quotient
                (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u) (B :=
                Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u))
                ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
          Type u))
        (⇑(CommRingCat.Hom.hom
              (Iso.inv
                ((Scheme.Hom.ker f).subschemeObjIso (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
          (a : (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, ⋯⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩)) : Type u)) →
            (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
        (⇑(CommRingCat.Hom.hom
                (CommRingCat.ofHom
                  (Ideal.Quotient.mk
                    ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
              (↑Γ(Y, ⊤) : Type u) →+*
                (↑(CommRingCat.of
                      (HasQuotient.Quotient
                        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u)
                        (B :=
                        Ideal
                          (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u))
                        ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
                  Type u)) :
          (a : (↑Γ(Y, ⊤) : Type u)) →
            (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, ⋯⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩)) : Type u))))

Tactic:
(ConcreteCategory.bijective_of_isIso _).2.comp
    ((ConcreteCategory.bijective_of_isIso _).2.comp Ideal.Quotient.mk_surjective)

Premises used: Ideal.Quotient.mk_surjective, And.right, Function.Surjective.comp, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
⊢ Function.Surjective (α := (↑Γ(Y, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (Function.comp (β := (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
      (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.toImage f) ⊤)) :
        (a : (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
      (Function.comp (β :=
        (↑(CommRingCat.of
              (HasQuotient.Quotient
                (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u) (B :=
                Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u))
                ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
          Type u))
        (⇑(CommRingCat.Hom.hom
              (Iso.inv
                ((Scheme.Hom.ker f).subschemeObjIso (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
          (a : (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, ⋯⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩)) : Type u)) →
            (↑Γ((Scheme.Hom.ker f).subscheme, ⊤) : Type u))
        (⇑(CommRingCat.Hom.hom
                (CommRingCat.ofHom
                  (Ideal.Quotient.mk
                    ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
              (↑Γ(Y, ⊤) : Type u) →+*
                (↑(CommRingCat.of
                      (HasQuotient.Quotient
                        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u)
                        (B :=
                        Ideal
                          (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u))
                        ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)))) :
                  Type u)) :
          (a : (↑Γ(Y, ⊤) : Type u)) →
            (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, ⋯⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩)) : Type u))))

Tactic:
exact (ConcreteCategory.bijective_of_isIso _).2.comp
    ((ConcreteCategory.bijective_of_isIso _).2.comp Ideal.Quotient.mk_surjective)

Premises used: Ideal.Quotient.mk_surjective, And.right, Function.Surjective.comp, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
mp :
  IsClosedImmersion f →
    ∃ (I : Ideal (↑R : Type u)) (e : X ≅ Spec (CommRingCat.of ((↑R : Type u) ⧸ I))),
      f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))
mpr :
  (∃ (I : Ideal (↑R : Type u)) (e : X ≅ Spec (CommRingCat.of ((↑R : Type u) ⧸ I))),
      f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) →
    IsClosedImmersion f
⊢ IsClosedImmersion f ↔
    ∃ (I : Ideal (↑R : Type u)) (e : X ≅ Spec (CommRingCat.of ((↑R : Type u) ⧸ I))),
      f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
⊢ IsAffine X

Tactic:
obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f

Premises used: AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
⊢ Function.Surjective (α := (↑Γ(Spec R, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Spec R, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f

Premises used: AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ :
  Function.Surjective (α := (↑Γ(Spec R, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Spec R, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ ∃ (I : Ideal (↑R : Type u)) (e : X ≅ Spec (CommRingCat.of ((↑R : Type u) ⧸ I))),
    f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
⟨RingHom.ker φ.1, Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso
        (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩

Premises used: RingEquiv.ofBijective, CategoryTheory.Iso.op, RingEquiv.toCommRingCatIso, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Iso.trans, Exists.intro, RingHom.kerLift, CategoryTheory.Functor.mapIso, RingHom.ker, CommRingCat.Hom.hom'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ :
  Function.Surjective (α := (↑Γ(Spec R, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop f)) :
      (a : (↑Γ(Spec R, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
mp :
  Function.Bijective (α := HasQuotient.Quotient (↑R : Type u) (B := Ideal (↑R : Type u)) (RingHom.ker φ.hom')) (β :=
    (↑Γ(X, ⊤) : Type u)) (⇑φ.hom'.kerLift : (a : (↑R : Type u) ⧸ RingHom.ker φ.hom') → (↑Γ(X, ⊤) : Type u))
mp₁ :
  f =
    (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯)).op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))
⊢ ∃ (I : Ideal (↑R : Type u)) (e : X ≅ Spec (CommRingCat.of ((↑R : Type u) ⧸ I))),
    f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
refine ⟨RingHom.ker φ.1, Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso
        (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩