awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
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)
⊢ JacobsonSpace.{u} ↥(Spec S)
have this₁ : IsJacobsonRing.{u} (↑R : Type u)
Tactic: have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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)
have refine_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage
Tactic: refine .of_functor F ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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
⊢ EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ Scheme.Spec X)
have 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)
Tactic: refine .of_functor F ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
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} F.essImage
have this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
Tactic: have : Q'.EssentiallySmall := CommRingCat.essentiallySmall_of_finiteType fun S ↦ id
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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
have rw : ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage.unop
Tactic: rw [← ObjectProperty.essentiallySmall_unop_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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
have refine : F.essImage.unop ≤ ObjectProperty.isoClosure fun (x : CommRingCat.{u}) ↦ x ∈ Set.range (unop ∘ F.obj)
Tactic: refine .of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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} F.essImage
have refine_1 : ObjectProperty.EssentiallySmall.{u, u, u + 1} (C := CommRingCat) fun (x : CommRingCat.{u}) ↦
  x ∈ Set.range (unop ∘ F.obj)
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⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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)
have 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))
Tactic: refine CommRingCat.essentiallySmall_of_localizationAway (Q := Q'.isoClosure) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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)
have 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)
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hqU, -⟩ :=
        X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ <| S.hom q) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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 (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)
have 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)
Tactic: obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
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))
⊢ ∃ (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)
have this₁ : LocallyOfFiniteType S.toComma (P := P) (Q := ⊤) (W := ⊤).hom
Tactic: have : LocallyOfFiniteType S.hom := hP _ S.prop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (hypothesis)
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
⊢ ∃ (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))
have 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)
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 _)) _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: choose f hqf hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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))
have refine_1 : Eq.{u + 1} (α := Opens (PrimeSpectrum (↑((unop ∘ F.obj) S) : Type u)))
  (⨆ (i : ↥(Spec (unop (F.obj S)))), PrimeSpectrum.basicOpen (f i)) ⊤
Tactic: refine ⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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)) ⊤
⊢ ∃ (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))
have refine_1₁ : ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
Tactic: refine ⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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)
have 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) sorry))
Tactic: refine ⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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) ⋯))
have refine_2 : ∀ (S : P.CostructuredArrow ⊤ Scheme.Spec X),
  (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S →
    ∀ (e : F.obj S ≅ R),
      Scheme.Spec.map e.hom ≫
          Comma.hom
            (MorphismProperty.Comma.toComma (P := P) (Q := ⊤) (W := ⊤)
              (MorphismProperty.CostructuredArrow.mk (P := P) ⊤
                (↑(Subtype.mk (p := fun (f : Spec (unop R) ⟶ X) ↦ P f)
                      (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom) sorry) :
                  Spec (unop R) ⟶ X)
                sorry)) =
        S.toComma (P := P) (Q := ⊤) (W := ⊤).hom
Tactic: refine fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FiniteType (goal)
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 :
  ∀ (S : P.CostructuredArrow ⊤ Scheme.Spec X),
    (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S →
      ∀ (e : F.obj S ≅ R),
        Scheme.Spec.map e.hom ≫
            Comma.hom
              (MorphismProperty.Comma.toComma (P := P) (Q := ⊤) (W := ⊤)
                (MorphismProperty.CostructuredArrow.mk (P := P) ⊤
                  (↑(Subtype.mk (p := fun (f : Spec (unop R) ⟶ X) ↦ P f)
                        (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯) :
                    Spec (unop R) ⟶ X)
                  ⋯)) =
          S.toComma (P := P) (Q := ⊤) (W := ⊤).hom
⊢ 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) ⋯))
have refine_2₁ : ∀ (S : P.CostructuredArrow ⊤ Scheme.Spec X),
  (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S →
    ∀ (e : F.obj S ≅ R), P (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom)
Tactic: refine fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ @Flat = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  Flat f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ Flat f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
have h : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
  affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
Tactic: rw [flat_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
⊢ Flat f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
have h₁ : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
  ∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat
Tactic: rw [flat_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
⊢ Flat f
have refine : Flat (f ≫ Y.isoSpec.hom)
Tactic: refine (MorphismProperty.cancel_right_of_respectsIso @Flat _ Y.isoSpec.hom).mp ?_