awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : (∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsFinite (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)) ↔
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    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)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsFinite (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)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      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)
have inst : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
  Subsingleton.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Tactic: have inst (i) := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.injective.subsingleton
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
inst_3 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inst :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsFinite (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)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      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)
have inst₁ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
  IsReduced.{u} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Tactic: have inst (i) := isReduced_of_isOpenImmersion ((Y.affineCover.pullback₁ f).f i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
inst_3 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inst_4 :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced.{u} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsFinite (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)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      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)
have inst₁ : ∀ (i : Y.affineCover.I₀), JacobsonSpace.{u} ↥(Y.affineCover.X i)
Tactic: have inst (i) := JacobsonSpace.of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst_2 : JacobsonSpace.{u} ↥(Spec S)
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} [Subsingleton.{u + 1} ↥X] [IsReduced X] {f : X ⟶ Spec S}
      (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsFinite f ↔ LocallyOfFiniteType f)
  (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), IsFinite f ↔ LocallyOfFiniteType f
Tactic: wlog hX : ∃ R, X = Spec R generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst_2 : JacobsonSpace.{u} ↥(Spec S)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [Subsingleton.{u + 1} ↥X] [IsReduced X] {f : X ⟶ Spec S}
        (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsFinite f ↔ LocallyOfFiniteType f)
    (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), IsFinite f ↔ LocallyOfFiniteType f
⊢ IsFinite f ↔ LocallyOfFiniteType f
have wlog : ∀ {X : Scheme.{u}} [Subsingleton.{u + 1} ↥X] [IsReduced X] {f : X ⟶ Spec S} (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
  IsFinite f ↔ LocallyOfFiniteType f
Tactic: wlog hX : ∃ R, X = Spec R generalizing X
Cleared hypotheses: X, inst, inst_1, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst_2 : JacobsonSpace.{u} ↥(Spec S)
this :
  ∀ {X : Scheme.{u}} [Subsingleton.{u + 1} ↥X] [IsReduced X] {f : X ⟶ Spec S}
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsFinite f ↔ LocallyOfFiniteType f
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso (P := @IsFinite) X.isoSpec.inv,
      ← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType) X.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X : Scheme
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst_2 : JacobsonSpace.{u} ↥(Spec S)
this :
  ∀ {X : Scheme.{u}} [Subsingleton.{u + 1} ↥X] [IsReduced X] {f : X ⟶ Spec S}
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsFinite f ↔ LocallyOfFiniteType f
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)
have inst : Subsingleton.{u + 1} ↥(Spec Γ(X, ⊤))
Tactic: have inst := X.isoSpec.inv.isOpenEmbedding.injective.subsingleton
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
X : Scheme
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
f : X ⟶ Spec S
hX : ∃ (R : CommRingCat.{u}), X = Spec R
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inl : IsEmpty.{u + 1} ↥X → (IsFinite f ↔ LocallyOfFiniteType f)
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
X : Scheme
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
f : X ⟶ Spec S
hX : ∃ (R : CommRingCat.{u}), X = Spec R
inl : IsEmpty.{u + 1} ↥X → (IsFinite f ↔ LocallyOfFiniteType f)
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : Nonempty.{u + 1} ↥X → (IsFinite f ↔ LocallyOfFiniteType f)
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
X : Scheme
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
f : X ⟶ Spec S
hX : ∃ (R : CommRingCat.{u}), X = Spec R
h : Nonempty.{u + 1} ↥X
⊢ IsFinite f ↔ LocallyOfFiniteType f
have this : IrreducibleSpace.{u} ↥X
Tactic: have : IrreducibleSpace X := ⟨‹_›⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
X : Scheme
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
f : X ⟶ Spec S
hX : ∃ (R : CommRingCat.{u}), X = Spec R
h : Nonempty.{u + 1} ↥X
this : IrreducibleSpace.{u} ↥X
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : ∀ (R : CommRingCat.{u}) [Subsingleton.{u + 1} ↥(Spec R)] [IsReduced.{u} (Spec R)] {f : Spec R ⟶ Spec S},
  Nonempty.{u + 1} ↥(Spec R) → ∀ (this : IrreducibleSpace.{u} ↥(Spec R)), IsFinite f ↔ LocallyOfFiniteType f
Tactic: obtain ⟨R, rfl⟩ := hX
Cleared hypotheses: X, inst_1, inst_2, f, hX, h, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
R : CommRingCat
inst_1 : Subsingleton.{u + 1} ↥(Spec R)
inst_2 : IsReduced.{u} (Spec R)
f : Spec R ⟶ Spec S
h : Nonempty.{u + 1} ↥(Spec R)
this : IrreducibleSpace.{u} ↥(Spec R)
⊢ IsFinite f ↔ LocallyOfFiniteType f
have this₁ : IsDomain.{u} (↑R : Type u)
Tactic: have : IsDomain R := (affine_isIntegral_iff R).mp (isIntegral_of_irreducibleSpace_of_isReduced _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
R : CommRingCat
inst_1 : Subsingleton.{u + 1} ↥(Spec R)
inst_2 : IsReduced.{u} (Spec R)
f : Spec R ⟶ Spec S
h : Nonempty.{u + 1} ↥(Spec R)
this_1 : IrreducibleSpace.{u} ↥(Spec R)
this : IsDomain.{u} (↑R : Type u)
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : ∀ (φ : S ⟶ R), IsFinite (Spec.map φ) ↔ LocallyOfFiniteType (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
R : CommRingCat
inst_1 : Subsingleton.{u + 1} ↥(Spec R)
inst_2 : IsReduced.{u} (Spec R)
h : Nonempty.{u + 1} ↥(Spec R)
this_1 : IrreducibleSpace.{u} ↥(Spec R)
this : IsDomain.{u} (↑R : Type u)
φ : S ⟶ R
⊢ IsFinite (Spec.map φ) ↔ LocallyOfFiniteType (Spec.map φ)
have inr : (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
Tactic: rw [IsFinite.SpecMap_iff, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
R : CommRingCat
inst_1 : Subsingleton.{u + 1} ↥(Spec R)
inst_2 : IsReduced.{u} (Spec R)
h : Nonempty.{u + 1} ↥(Spec R)
this_1 : IrreducibleSpace.{u} ↥(Spec R)
this : IsDomain.{u} (↑R : Type u)
φ : S ⟶ R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
have this₁ : IsField.{u} (↑R : Type u)
Tactic: have := (PrimeSpectrum.t1Space_iff_isField (R := R)).mp (show T1Space (Spec R) by infer_instance)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
S : CommRingCat
inst : JacobsonSpace.{u} ↥(Spec S)
R : CommRingCat
inst_1 : Subsingleton.{u + 1} ↥(Spec R)
inst_2 : IsReduced.{u} (Spec R)
h : Nonempty.{u + 1} ↥(Spec R)
this_1 : IrreducibleSpace.{u} ↥(Spec R)
this_2 : IsDomain.{u} (↑R : Type u)
φ : S ⟶ R
this_3 : IsField.{u} (↑R : Type u)
this_4 : Field (↑R : Type u) := this_3.toField
this : Algebra (↑S : Type u) (↑R : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
have this₁ : IsJacobsonRing.{u} (↑S : Type u)
Tactic: have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : JacobsonSpace.{u} ↥Y
inst_1 : LocallyOfFiniteType f
x : ↥X
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
⊢ Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (closedPoints ↥Y)) x
have this : IsClosedImmersion (X.fromSpecResidueField x)
Tactic: have := isClosed_singleton_iff_isClosedImmersion.mp hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : JacobsonSpace.{u} ↥Y
inst_1 : LocallyOfFiniteType f
x : ↥X
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
this : IsClosedImmersion (X.fromSpecResidueField x)
⊢ Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (closedPoints ↥Y)) x
have this₁ : IsFinite (X.fromSpecResidueField x ≫ f)
Tactic: have := (isFinite_iff_locallyOfFiniteType_of_jacobsonSpace
    (f := X.fromSpecResidueField x ≫ f)).mpr inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X : Scheme
inst : JacobsonSpace.{u} ↥X
x : ↥X
⊢ IsClosed (X := ↥X) {x} ↔ LocallyOfFiniteType (X.fromSpecResidueField x)
have mp : IsClosed (X := ↥X) {x} → LocallyOfFiniteType (X.fromSpecResidueField x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X : Scheme
inst : JacobsonSpace.{u} ↥X
x : ↥X
mp : IsClosed (X := ↥X) {x} → LocallyOfFiniteType (X.fromSpecResidueField x)
⊢ IsClosed (X := ↥X) {x} ↔ LocallyOfFiniteType (X.fromSpecResidueField x)
have mpr : LocallyOfFiniteType (X.fromSpecResidueField x) → IsClosed (X := ↥X) {x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFinitePresentation =
    affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  LocallyOfFinitePresentation f ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFinitePresentation f ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) 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)).FinitePresentation) ↔
  affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
Tactic: rw [locallyOfFinitePresentation_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X_1 Y_1 : 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)).FinitePresentation) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ LocallyOfFinitePresentation f ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) 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)).FinitePresentation) ↔
  ∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens},
        IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FinitePresentation
Tactic: rw [locallyOfFinitePresentation_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
⊢ LocallyOfFiniteType f
have hf₁ : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
Tactic: rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ LocallyOfFiniteType f
have rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Tactic: rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
have refine : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} (hf : f.FinitePresentation), f.FiniteType
Tactic: refine affineLocally_le (fun hf ↦ ?_) f hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
      (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
      IsLocallyConstructible (X := ↥Y) (⇑f '' s))
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstructible (X := ↥Y) (⇑f '' s)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
        (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        IsLocallyConstructible (X := ↥Y) (⇑f '' s))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstructible (X := ↥Y) (⇑f '' s)
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
  (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstructible (X := ↥Y) (⇑f '' s)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, hf, inst, s, hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)
have inr : ∀ (i : Y.affineCover.I₀),
  IsLocallyConstructible (X := (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
Tactic: refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
⊢ IsLocallyConstructible (X := (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
have inst : LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
  (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: have inst : LocallyOfFinitePresentation (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ IsLocallyConstructible (X := (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ x ∈ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y)) ⁻¹' ⇑f '' s)
have inst₁ : QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
  (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: have inst : QuasiCompact (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance