awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
⟨φ.1.kerLift_injective, Ideal.Quotient.lift_surjective_of_surjective _ _
        (h₂.comp (Scheme.ΓSpecIso R).commRingCatIsoToRingEquiv.symm.surjective)⟩

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingEquiv.surjective, Ideal.Quotient.lift_surjective_of_surjective, AlgebraicGeometry.Scheme.ΓSpecIso, RingHom.kerLift_injective, And.intro, Function.Surjective.comp, Function.Bijective, RingEquiv.symm, 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
⊢ 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:
exact ⟨φ.1.kerLift_injective, Ideal.Quotient.lift_surjective_of_surjective _ _
        (h₂.comp (Scheme.ΓSpecIso R).commRingCatIsoToRingEquiv.symm.surjective)⟩
-- 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 :
  f =
    X.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')) ≫
          (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯)).hom)
⊢ f =
    (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯)).op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.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]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Iso.op_hom, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.Spec_map, CategoryTheory.Functor.mapIso_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 : f = X.isoSpec.hom ≫ Spec.map φ
⊢ f =
    X.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')) ≫
          (RingEquiv.toCommRingCatIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯)).hom)

Tactic:
change f = X.isoSpec.hom ≫ Spec.map φ

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Spec.map, CategoryTheory.Iso.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 : f = f ≫ Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv
⊢ f = X.isoSpec.hom ≫ Spec.map φ

Tactic:
simp only [Scheme.isoSpec, asIso_hom, Spec.map_comp, ← Scheme.toSpecΓ_naturality_assoc,
        ← SpecMap_ΓSpecIso_hom, φ]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Spec.map_comp, CategoryTheory.asIso_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
⊢ f = f ≫ Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
R : CommRingCat
I : Ideal (↑R : Type u)
e : X ≅ Spec (CommRingCat.of ((↑R : Type u) ⧸ I))
⊢ IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
⊢ IsZariskiLocalAtTarget @IsClosedImmersion

Tactic:
eq_inf ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.IsClosedImmersion.eq_inf, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
⊢ HasAffineProperty (@IsClosedImmersion) (AffineTargetMorphismProperty.of @IsClosedImmersion)

Tactic:
HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion

Premises used: AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget, AlgebraicGeometry.IsClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
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
⊢ 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))

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion

Premises used: AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget, AlgebraicGeometry.IsClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
x x_1 : Scheme
x_2 : x ⟶ x_1
h : IsAffine x_1
⊢ AffineTargetMorphismProperty.of (@IsClosedImmersion) x_2 →
    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))

Tactic:
apply isAffine_surjective_of_isAffine

Premises used: AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
x x_1 : Scheme
x_2 : x ⟶ x_1
h : 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:
refine ⟨fun ⟨h₁, h₂⟩ ↦ of_surjective_of_isAffine _ h₂, by apply isAffine_surjective_of_isAffine⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
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))
⊢ 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))

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion]

Premises used: AlgebraicGeometry.IsClosedImmersion, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ 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:
targetAffineLocally_affineAnd_iff' RingHom.surjective_respectsIso _

Premises used: AlgebraicGeometry.affineAnd, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', RingHom.surjective_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ 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:
exact targetAffineLocally_affineAnd_iff' RingHom.surjective_respectsIso _

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff', RingHom.surjective_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
inst : IsClosedImmersion f
⊢ 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) (app f U)) :
      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))

Tactic:
(isClosedImmersion_iff_isAffineHom.mp ‹_›).2 U hU

Premises used: AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, And.right, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
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))
⊢ MorphismProperty.IsStableUnderBaseChange @IsClosedImmersion

Tactic:
apply HasAffineProperty.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
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))
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))
⊢ 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 AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
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
hP' :
  ∀ [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))
⊢ ∀ [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:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
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
hP' :
  ∀ [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))
⊢ ∀ [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:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
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
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))
⊢ 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:
⟨ha, hsurj⟩