awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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) (Scheme.Hom.stalkMap f x) :
          (a : (↑(Y.presheaf.stalk (f x)) : 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) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
              (a : (↑(Y.presheaf.obj (op ⊤)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            g :
          (↑(Y.presheaf.stalk (f x)) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
⊢ Eq (α := (↑(Y.presheaf.stalk (f x)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
          (a : (↑(Y.presheaf.obj (op ⊤)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
        g :
      (↑(Y.presheaf.stalk (f x)) : Type u))
    (0 : (↑(Y.presheaf.stalk (f x)) : Type u))
have 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))
Tactic: rw [TopCat.Presheaf.Γgerm, Scheme.Hom.germ_stalkMap_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
have 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))
Tactic: refine ⟨isAffine_of_isAffineHom f, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : IsClosedImmersion f
⊢ 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))
have 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)))
Tactic: simp only [← f.toImage_imageι, Scheme.Hom.comp_appTop, CommRingCat.hom_comp, RingHom.coe_comp,
    Scheme.Hom.image, Scheme.Hom.imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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.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)))
have 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) ⊤ sorry) : Y.Opens)) : Type u) (B :=
              Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ sorry) : Y.Opens)) : Type u))
              ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ sorry)))) :
        Type u))
      (⇑(CommRingCat.Hom.hom
            (Iso.inv
              ((Scheme.Hom.ker f).subschemeObjIso (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ sorry)))) :
        (a : (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, sorry⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, sorry⟩)) : 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) ⊤ sorry)))) :
            (↑Γ(Y, ⊤) : Type u) →+*
              (↑(CommRingCat.of
                    (HasQuotient.Quotient
                      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ sorry) : Y.Opens)) : Type u) (B :=
                      Ideal
                        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ sorry) : Y.Opens)) : Type u))
                      ((Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ sorry)))) :
                Type u)) :
        (a : (↑Γ(Y, ⊤) : Type u)) →
          (↑(CommRingCat.of ((↑Γ(Y, (↑⟨⊤, sorry⟩ : Y.Opens)) : Type u) ⧸ (Scheme.Hom.ker f).ideal ⟨⊤, sorry⟩)) : Type u))))
Tactic: rw [Scheme.Hom.appTop, Scheme.Hom.appTop, f.ker.subschemeι_app ⟨⊤, isAffineOpen_top Y⟩,
    CommRingCat.hom_comp, RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
⊢ 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))
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : 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))
have h₁ : IsAffine X
Tactic: obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
have 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))
Tactic: refine ⟨RingHom.ker φ.1, Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso
        (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
⊢ ∃ (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))
have mp₁ : f =
  (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift sorry)).op).hom ≫
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))
Tactic: refine ⟨RingHom.ker φ.1, Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso
        (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ f =
    (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯)).op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))
have mp : f =
  X.isoSpec.hom ≫
    Spec.map
      (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')) ≫
        (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift sorry)).hom)
Tactic: simp only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map,
        Quiver.Hom.unop_op, Category.assoc, ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ f =
    X.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')) ≫
          (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯)).hom)
have mp : f = X.isoSpec.hom ≫ Spec.map φ
Tactic: change f = X.isoSpec.hom ≫ Spec.map φ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ f = X.isoSpec.hom ≫ Spec.map φ
have mp : f = f ≫ Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv
Tactic: simp only [Scheme.isoSpec, asIso_hom, Spec.map_comp, ← Scheme.toSpecΓ_naturality_assoc,
        ← SpecMap_ΓSpecIso_hom, φ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y Z : Scheme
⊢ HasAffineProperty @IsClosedImmersion fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1) (x_3 : IsAffine x_1),
  IsAffine x ∧
      Function.Surjective (α := (↑Γ(x_1, ⊤) : Type u_1)) (β := (↑Γ(x, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop x_2)) :
          (a : (↑Γ(x_1, ⊤) : Type u_1)) → (↑Γ(x, ⊤) : Type u_1)) ↔
    AffineTargetMorphismProperty.of (@IsClosedImmersion) x_2
Tactic: convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    IsAffineHom f ∧
      ∀ (U : Y.Opens),
        IsAffineOpen U →
          Function.Surjective (α := (↑Γ(Y, U) : Type u)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U)) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
have rw : targetAffineLocally
    (fun (X x : Scheme.{u}) (f : X ⟶ x) [IsAffine x] ↦
      IsAffine X ∧
        Function.Surjective (α := (↑Γ(x, ⊤) : 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 : (↑Γ(x, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)))
    f ↔
  IsAffineHom f ∧
    ∀ (U : Y.Opens),
      IsAffineOpen U →
        Function.Surjective (α := (↑Γ(Y, U) : Type u)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.app f U)) :
            (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
Tactic: rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y Z : Scheme
⊢ MorphismProperty.IsStableUnderBaseChange @IsClosedImmersion
have hP' : AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
  IsAffine X ∧
    Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f)) :
        (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
Tactic: apply HasAffineProperty.isStableUnderBaseChange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X Y Z : Scheme
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
have this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
  IsAffine X ∧
    Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f)) :
        (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
Tactic: haveI := HasAffineProperty.isLocal_affineProperty @IsClosedImmersion
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
have hP' : ∀ ⦃X Y S : Scheme.{u_1}⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
  IsAffine Y ∧
      Function.Surjective (α := (↑Γ(S, ⊤) : Type u_1)) (β := (↑Γ(Y, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop g)) :
          (a : (↑Γ(S, ⊤) : Type u_1)) → (↑Γ(Y, ⊤) : Type u_1)) →
    IsAffine.{u_1} (Limits.pullback f g) ∧
      Function.Surjective (α := (↑Γ(X, ⊤) : Type u_1)) (β := (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := Γ(Limits.pullback f g, ⊤)) (Scheme.Hom.appTop (Limits.pullback.fst f g))) :
          (a : (↑Γ(X, ⊤) : Type u_1)) → (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
Tactic: apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X_1 Y_1 Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ IsAffine Y ∧
      Function.Surjective (α := (↑Γ(S, ⊤) : Type u_1)) (β := (↑Γ(Y, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop g)) :
          (a : (↑Γ(S, ⊤) : Type u_1)) → (↑Γ(Y, ⊤) : Type u_1)) →
    IsAffine.{u_1} (Limits.pullback f g) ∧
      Function.Surjective (α := (↑Γ(X, ⊤) : Type u_1)) (β := (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := Γ(Limits.pullback f g, ⊤)) (Scheme.Hom.appTop (Limits.pullback.fst f g))) :
          (a : (↑Γ(X, ⊤) : Type u_1)) → (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
have hP' : ∀ (ha : IsAffine Y)
  (hsurj :
    Function.Surjective (α := (↑Γ(S, ⊤) : Type u_1)) (β := (↑Γ(Y, ⊤) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop g)) :
        (a : (↑Γ(S, ⊤) : Type u_1)) → (↑Γ(Y, ⊤) : Type u_1))),
  IsAffine.{u_1} (Limits.pullback f g) ∧
    Function.Surjective (α := (↑Γ(X, ⊤) : Type u_1)) (β := (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := Γ(Limits.pullback f g, ⊤)) (Scheme.Hom.appTop (Limits.pullback.fst f g))) :
        (a : (↑Γ(X, ⊤) : Type u_1)) → (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
Tactic: ⟨ha, hsurj⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X_1 Y_1 Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ LocallyOfFiniteType f
have rw : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Tactic: rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType,
    ← and_iff_right (inferInstance : IsAffineHom f) (b := affineLocally _ _),
    ← targetAffineLocally_affineAnd_iff_affineLocally RingHom.finiteType_isLocal]