awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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))
obtain :
  ∀ (f : (↑(unop S.toComma (P := P) (Q := ⊤) (W := ⊤).left) : Type u))
    (hqf : q ∈ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u))))
    (hfU :
      (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u))) ⊆
        (↑(S.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⁻¹ᵁ U) : Set ↥(Scheme.Spec.obj S.left))),
    ∃ (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 ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen

Premises used: CategoryTheory.Comma.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.MorphismProperty.Comma.toComma, TopologicalSpace.Opens.isOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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)))
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 S.toComma (P := P) (Q := ⊤) (W := ⊤).left) : Type u)
hqf : q ∈ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u)))
hfU :
  (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u))) ⊆
    (↑(S.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⁻¹ᵁ U) : Set ↥(Scheme.Spec.obj S.left))
⊢ LocallyOfFiniteType S.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
have : LocallyOfFiniteType S.hom := hP _ S.prop
-- 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'
S : P.CostructuredArrow ⊤ Scheme.Spec X
q : ↥(Spec (unop (F.obj S)))
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 S.toComma (P := P) (Q := ⊤) (W := ⊤).left) : Type u)
hqf : q ∈ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u)))
hfU :
  (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u))) ⊆
    (↑(S.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⁻¹ᵁ U) : Set ↥(Scheme.Spec.obj S.left))
this : LocallyOfFiniteType S.toComma (P := P) (Q := ⊤) (W := ⊤).hom
⊢ ∃ (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:
⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩

Premises used: CategoryTheory.Comma.hom, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.MorphismProperty.Comma.toComma, AlgebraicGeometry.Scheme.Hom.finiteType_appLE, And.intro, Exists.intro, rfl, AlgebraicGeometry.IsAffineOpen.Spec_basicOpen
-- 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'
S : P.CostructuredArrow ⊤ Scheme.Spec X
q : ↥(Spec (unop (F.obj S)))
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 S.toComma (P := P) (Q := ⊤) (W := ⊤).left) : Type u)
hqf : q ∈ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u)))
hfU :
  (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum (↑(unop S.left) : Type u))) ⊆
    (↑(S.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⁻¹ᵁ U) : Set ↥(Scheme.Spec.obj S.left))
this : LocallyOfFiniteType S.toComma (P := P) (Q := ⊤) (W := ⊤).hom
⊢ ∃ (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:
exact ⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩
-- 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)))),
    ∃ (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:
have (q : Spec (F.obj S).unop) : ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧
        Q' Γ(Spec (F.obj S).unop, PrimeSpectrum.basicOpen f) := by
      obtain ⟨_, ⟨U, hU, rfl⟩, hqU, -⟩ :=
        X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ <| S.hom q) isOpen_univ
      obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen
      have : LocallyOfFiniteType S.hom := hP _ S.prop
      exact ⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩
-- 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'
S : P.CostructuredArrow ⊤ Scheme.Spec X
this :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    ∃ (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)
refine_1 :
  ∀ (f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u))
    (hqf :
      ∀ (q : ↥(Spec (unop (F.obj S)))),
        Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q)
    (hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))),
    ∃ (s : Set (↑((unop ∘ F.obj) S) : Type u)),
      Eq (α := Ideal (↑((unop ∘ F.obj) S) : Type u)) (Ideal.span s) ⊤ ∧
        ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))
⊢ ∃ (s : Set (↑((unop ∘ F.obj) S) : Type u)),
    Eq (α := Ideal (↑((unop ∘ F.obj) S) : Type u)) (Ideal.span s) ⊤ ∧
      ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
choose f hqf hf using this
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∃ (s : Set (↑((unop ∘ F.obj) S) : Type u)),
    Eq (α := Ideal (↑((unop ∘ F.obj) S) : Type u)) (Ideal.span s) ⊤ ∧
      ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩

Premises used: Iff.mpr, Set.forall_mem_range, PrimeSpectrum.iSup_basicOpen_eq_top_iff, And.intro, Exists.intro, Iff.mp, Set.range
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
refine_1 :
  Eq.{u + 1} (α := Opens (PrimeSpectrum (↑((unop ∘ F.obj) S) : Type u)))
    (⨆ (i : ↥(Spec (unop (F.obj S)))), PrimeSpectrum.basicOpen (f i)) ⊤
refine_1₁ : ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
⊢ ∃ (s : Set (↑((unop ∘ F.obj) S) : Type u)),
    Eq (α := Ideal (↑((unop ∘ F.obj) S) : Type u)) (Ideal.span s) ⊤ ∧
      ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
refine ⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ Eq.{u + 1} (α := Opens (PrimeSpectrum (↑((unop ∘ F.obj) S) : Type u)))
    (⨆ (i : ↥(Spec (unop (F.obj S)))), PrimeSpectrum.basicOpen (f i)) ⊤

Tactic:
top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, hqf _⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_iSup, top_le_iff, Exists.intro, Iff.mp
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ Eq.{u + 1} (α := Opens (PrimeSpectrum (↑((unop ∘ F.obj) S) : Type u)))
    (⨆ (i : ↥(Spec (unop (F.obj S)))), PrimeSpectrum.basicOpen (f i)) ⊤

Tactic:
exact top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, hqf _⟩

Premises used: top_le_iff, Iff.mp
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
refine_1 : ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
dsimp
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
fun q ↦ ⟨_, hf q, ⟨(IsLocalization.algEquiv (.powers (f q)) _
        ((Spec.structureSheaf _).obj.obj (op _))).toRingEquiv.toCommRingCatIso⟩⟩

Premises used: AlgebraicGeometry.Spec, CommRingCat.carrier, PrimeSpectrum.basicOpen, RingEquiv.toCommRingCatIso, Localization.Away, CategoryTheory.ObjectProperty.FullSubcategory.obj, Nonempty.intro, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, IsLocalization.algEquiv, Submonoid.powers, CategoryTheory.ObjectProperty.isoClosure, AlgEquiv.toRingEquiv, Exists.intro, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.Spec.structureSheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Opposite.unop, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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
f : (q : ↥(Spec (unop (F.obj S)))) → (↑(unop (F.obj S)) : Type u)
hqf :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    Membership.mem (γ := Opens (PrimeSpectrum (↑(unop (F.obj S)) : Type u))) (PrimeSpectrum.basicOpen (f q)) q
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
exact fun q ↦ ⟨_, hf q, ⟨(IsLocalization.algEquiv (.powers (f q)) _
        ((Spec.structureSheaf _).obj.obj (op _))).toRingEquiv.toCommRingCatIso⟩⟩
-- 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
R : 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 ≅ R)

Tactic:
⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, CategoryTheory.MorphismProperty.CostructuredArrow.mk, inferInstance, Exists.intro, Top.top, Subtype.val, CategoryTheory.ObjectProperty.EssentiallySmall.mk, Subtype.property
-- 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
R : CommRingCatᵒᵖ
refine_2 :
  LE.le.{u + 1} (α := ObjectProperty (P.CostructuredArrow ⊤ Scheme.Spec X))
    (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R))
    (ObjectProperty.isoClosure
      (ObjectProperty.ofObj fun (f : { f : Spec (unop R) ⟶ X // P f }) ↦
        MorphismProperty.CostructuredArrow.mk (P := P) ⊤ (↑f : Spec (unop R) ⟶ X) ⋯))
⊢ 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 ≅ R)

Tactic:
refine ⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩
-- 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
R : CommRingCatᵒᵖ
⊢ LE.le.{u + 1} (α := ObjectProperty (P.CostructuredArrow ⊤ Scheme.Spec X))
    (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R))
    (ObjectProperty.isoClosure
      (ObjectProperty.ofObj fun (f : { f : Spec (unop R) ⟶ X // P f }) ↦
        MorphismProperty.CostructuredArrow.mk (P := P) ⊤ (↑f : Spec (unop R) ⟶ X) ⋯))

Tactic:
fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, _private.0.AlgebraicGeometry.essentiallySmall_costructuredArrow_Spec.match_2, trivial, CategoryTheory.MorphismProperty.CostructuredArrow.mk, Nonempty.intro, CategoryTheory.ObjectProperty.ofObj.mk, CategoryTheory.MorphismProperty.CostructuredArrow.isoMk, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, Top.top, Subtype.val, Subtype.property