awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst_3 :
  LocallyOfFiniteType (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst_4 : JacobsonSpace.{u} ↥Y
inst : JacobsonSpace.{u} ↥(Y.affineCover.X i)
e : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) ≃ₜ
  (↑(Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i)) :
    Type u) :=
  ⋯.toHomeomorph
⊢ JacobsonSpace.{u} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst_3 :
  LocallyOfFiniteType (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst_4 : JacobsonSpace.{u} ↥Y
inst : JacobsonSpace.{u} ↥(Y.affineCover.X i)
e : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) ≃ₜ
  (↑(Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i)) :
    Type u) :=
  ⋯.toHomeomorph
this : JacobsonSpace.{u} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))

Tactic:
.of_isClosedEmbedding e.symm.isClosedEmbedding

Premises used: Homeomorph.symm, JacobsonSpace.of_isClosedEmbedding, Homeomorph.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst_3 :
  LocallyOfFiniteType (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst_4 : JacobsonSpace.{u} ↥Y
inst : JacobsonSpace.{u} ↥(Y.affineCover.X i)
e : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) ≃ₜ
  (↑(Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i)) :
    Type u) :=
  ⋯.toHomeomorph
this : JacobsonSpace.{u} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))

Tactic:
exact .of_isClosedEmbedding e.symm.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)], JacobsonSpace.{u} ↥X
⊢ JacobsonSpace.{u} ↥X

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥(Spec R)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
wlog :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
⊢ JacobsonSpace.{u} ↥X

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥(Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ JacobsonSpace.{u} ↥(Spec R)

Tactic:
have inst : JacobsonSpace (Spec R) := ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥(Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : JacobsonSpace.{u} ↥(Spec R)
inr : ∀ (i : X.affineCover.I₀), JacobsonSpace.{u} ↥(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ JacobsonSpace.{u} ↥X

Tactic:
rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]

Premises used: AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, TopologicalSpace.IsOpenCover.jacobsonSpace_iff, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥(Spec R)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : JacobsonSpace.{u} ↥(Spec R)
i : X.affineCover.I₀
⊢ JacobsonSpace.{u} ↥(X.affineCover.X i)

Tactic:
have := this _ (X.affineCover.f i ≫ f) ⟨_, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥(Spec R)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : JacobsonSpace.{u} ↥(Spec R)
i : X.affineCover.I₀
this : JacobsonSpace.{u} ↥(X.affineCover.X i)
e : ↥(X.affineCover.X i) ≃ₜ (↑(Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) : Type u) := ⋯.toHomeomorph
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange (X.affineCover.f i))

Tactic:
.of_isClosedEmbedding e.symm.isClosedEmbedding

Premises used: Homeomorph.symm, JacobsonSpace.of_isClosedEmbedding, Homeomorph.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥(Spec R)
this_1 :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥(Spec R)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), JacobsonSpace.{u} ↥X
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : JacobsonSpace.{u} ↥(Spec R)
i : X.affineCover.I₀
this : JacobsonSpace.{u} ↥(X.affineCover.X i)
e : ↥(X.affineCover.X i) ≃ₜ (↑(Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) : Type u) := ⋯.toHomeomorph
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.opensRange (X.affineCover.f i))

Tactic:
exact .of_isClosedEmbedding e.symm.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥(Spec R)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f], JacobsonSpace.{u} ↥(Spec S)
⊢ JacobsonSpace.{u} ↥X

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyOfFiniteType f
obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)], JacobsonSpace.{u} ↥(Spec S)
⊢ JacobsonSpace.{u} ↥(Spec S)

Tactic:
obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f

Premises used: AlgebraicGeometry.Spec.homEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
have : RingHom.FiniteType φ.hom := HasRingHomProperty.Spec_iff.mp ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
⊢ Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsJacobsonRing.{u} (↑R : Type u)

Tactic:
have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this_1 : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : IsJacobsonRing.{u} (↑R : Type u)
⊢ JacobsonSpace.{u} ↥(Spec S)

Tactic:
PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mp (isJacobsonRing_of_finiteType (A := R))

Premises used: Iff.mp, isJacobsonRing_of_finiteType, PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
R : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this_1 : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : IsJacobsonRing.{u} (↑R : Type u)
⊢ JacobsonSpace.{u} ↥(Spec S)

Tactic:
exact PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mp (isJacobsonRing_of_finiteType (A := R))

Premises used: Iff.mp, isJacobsonRing_of_finiteType, PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ Scheme.Spec X)

Tactic:
.of_functor F ?_ ?_

Premises used: CategoryTheory.EssentiallySmall.of_functor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
refine_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage
refine_2 :
  ∀ (Y : CommRingCatᵒᵖ),
    ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := P.CostructuredArrow ⊤ Scheme.Spec X)
      fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ Y)
⊢ EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ Scheme.Spec X)

Tactic:
refine .of_functor F ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'

Tactic:
have : Q'.EssentiallySmall := CommRingCat.essentiallySmall_of_finiteType fun S ↦ id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
this :
  ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)
rw : ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage.unop
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage

Tactic:
rw [← ObjectProperty.essentiallySmall_unop_iff]

Premises used: CategoryTheory.ObjectProperty.essentiallySmall_unop_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
this :
  ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage.unop

Tactic:
.of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.of_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
this :
  ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)
refine : F.essImage.unop ≤ ObjectProperty.isoClosure fun (x : CommRingCat.{u}) ↦ x ∈ Set.range (unop ∘ F.obj)
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage.unop

Tactic:
refine .of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
this :
  ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)
⊢ F.essImage.unop ≤ ObjectProperty.isoClosure fun (x : CommRingCat.{u}) ↦ x ∈ Set.range (unop ∘ F.obj)

Tactic:
fun R ⟨S, e⟩ ↦ ⟨_, ⟨S, rfl⟩, ⟨e.some.unop⟩⟩

Premises used: Function.comp, Membership.mem, Nonempty.some, Nonempty.intro, _private.0.AlgebraicGeometry.essentiallySmall_costructuredArrow_Spec.match_1, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, Set.range, Opposite.unop, CategoryTheory.Functor.obj, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
this :
  ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)
⊢ F.essImage.unop ≤ ObjectProperty.isoClosure fun (x : CommRingCat.{u}) ↦ x ∈ Set.range (unop ∘ F.obj)

Tactic:
exact fun R ⟨S, e⟩ ↦ ⟨_, ⟨S, rfl⟩, ⟨e.some.unop⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
refine_1 :
  ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage

Tactic:
suffices ObjectProperty.EssentiallySmall.{u} (· ∈ Set.range (Opposite.unop ∘ F.obj)) by
      rw [← ObjectProperty.essentiallySmall_unop_iff]
      refine .of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_
      exact fun R ⟨S, e⟩ ↦ ⟨_, ⟨S, rfl⟩, ⟨e.some.unop⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)

Tactic:
CommRingCat.essentiallySmall_of_localizationAway (Q := Q'.isoClosure) ?_

Premises used: CommRingCat.essentiallySmall_of_localizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
refine_1 :
  ∀ S ∈ Set.range (unop ∘ F.obj),
    ∃ (s : Set (↑S : Type u)),
      Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
    x ∈ Set.range (unop ∘ F.obj)

Tactic:
refine CommRingCat.essentiallySmall_of_localizationAway (Q := Q'.isoClosure) ?_

Premises used: CommRingCat.essentiallySmall_of_localizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat :=
  fun (S : CommRingCat.{u}) ↦
    ∃ (R : CommRingCat.{u}),
      Membership.mem (γ := Set CommRingCat) (Set.range fun (U : X.Opens) ↦ Γ(X, U)) R ∧
        ∃ (f : R ⟶ S), (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
q : ↥(Spec (unop (F.obj S)))
obtain :
  ∀ (U : Opens ↥X) (hU : U ∈ X.affineOpens)
    (hqU :
      Membership.mem (α := ↥X) (↑U : Set ↥X)
        (S.toComma (P := P) (Q := ⊤) (W := ⊤).hom q :
          ↥(Functor.obj (Functor.fromPUnit X) S.toComma (P := P) (Q := ⊤) (W := ⊤).right))),
    ∃ (f : (↑(unop (F.obj S)) : Type u)),
      Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen f) q ∧
        Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)
⊢ ∃ (f : (↑(unop (F.obj S)) : Type u)),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen f) q ∧
      Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hqU, -⟩ :=
        X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ <| S.hom q) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Comma.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, CategoryTheory.MorphismProperty.Comma.toComma, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open