awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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 : (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)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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.I₀), JacobsonSpace.{u} ↥(Y.affineCover.X i)

Tactic:
have inst (i) := JacobsonSpace.of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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_5 :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced.{u} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst : ∀ (i : Y.affineCover.I₀), JacobsonSpace.{u} ↥(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)

Tactic:
forall_congr' fun i ↦ this ⟨_, rfl⟩

Premises used: Exists.intro, forall_congr', AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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_5 :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced.{u} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst : ∀ (i : Y.affineCover.I₀), JacobsonSpace.{u} ↥(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)

Tactic:
exact forall_congr' fun i ↦ this ⟨_, rfl⟩

Premises used: Exists.intro, forall_congr', rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
wlog hX : ∃ R, X = Spec R generalizing X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
inr : IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (P := @IsFinite) X.isoSpec.inv,
      ← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType) X.isoSpec.inv]

Premises used: AlgebraicGeometry.IsFinite, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.LocallyOfFiniteType, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ Subsingleton.{u + 1} ↥(Spec Γ(X, ⊤))

Tactic:
have inst := X.isoSpec.inv.isOpenEmbedding.injective.subsingleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X : Scheme
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst_3 : 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
inst : Subsingleton.{u + 1} ↥(Spec Γ(X, ⊤))
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)

Tactic:
this ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X : Scheme
inst_1 : Subsingleton.{u + 1} ↥X
inst_2 : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst_3 : 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
inst : Subsingleton.{u + 1} ↥(Spec Γ(X, ⊤))
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)

Tactic:
refine this ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)
inr : Nonempty.{u + 1} ↥X → (IsFinite f ↔ LocallyOfFiniteType f)
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
cases isEmpty_or_nonempty X

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, isEmpty_or_nonempty, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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 : IsEmpty.{u + 1} ↥X
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
⟨inferInstance, inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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 : IsEmpty.{u + 1} ↥X
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
exact ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ IrreducibleSpace.{u} ↥X

Tactic:
have : IrreducibleSpace X := ⟨‹_›⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
obtain ⟨R, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)
⊢ IsDomain.{u} (↑R : Type u)

Tactic:
have : IsDomain R := (affine_isIntegral_iff R).mp (isIntegral_of_irreducibleSpace_of_isReduced _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)
inr : ∀ (φ : S ⟶ R), IsFinite (Spec.map φ) ↔ LocallyOfFiniteType (Spec.map φ)
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
inr : (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
⊢ IsFinite (Spec.map φ) ↔ LocallyOfFiniteType (Spec.map φ)

Tactic:
rw [IsFinite.SpecMap_iff, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ T1Space.{u} ↥(Spec R)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ IsField.{u} (↑R : Type u)

Tactic:
have := (PrimeSpectrum.t1Space_iff_isField (R := R)).mp (show T1Space (Spec R) by infer_instance)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ IsJacobsonRing.{u} (↑S : Type u)

Tactic:
have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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_5 : Algebra (↑S : Type u) (↑R : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
this : IsJacobsonRing.{u} (↑S : Type u)
⊢ Module.Finite.{u, u} (↑S : Type u) (↑R : Type u) ↔ Algebra.FiniteType.{u, u} (↑S : Type u) (↑R : Type u)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ finite_of_finite_type_of_isJacobsonRing _ _⟩

Premises used: CommRingCat.carrier, finite_of_finite_type_of_isJacobsonRing, inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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_5 : Algebra (↑S : Type u) (↑R : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
this : IsJacobsonRing.{u} (↑S : Type u)
⊢ Module.Finite.{u, u} (↑S : Type u) (↑R : Type u) ↔ Algebra.FiniteType.{u, u} (↑S : Type u) (↑R : Type u)

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ finite_of_finite_type_of_isJacobsonRing _ _⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ IsClosedImmersion (X.fromSpecResidueField x)

Tactic:
have := isClosed_singleton_iff_isClosedImmersion.mp hx
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)
⊢ IsFinite (X.fromSpecResidueField x ≫ f)

Tactic:
have := (isFinite_iff_locallyOfFiniteType_of_jacobsonSpace
    (f := X.fromSpecResidueField x ≫ f)).mpr inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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_1 : IsClosedImmersion (X.fromSpecResidueField x)
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (closedPoints ↥Y)) x

Tactic:
simpa [Set.range_comp, Scheme.range_fromSpecResidueField] using
    (X.fromSpecResidueField x ≫ f).isClosedMap.isClosed_range

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.fromSpecResidueField, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.range_fromSpecResidueField, IsClosedMap.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X : Scheme
inst : JacobsonSpace.{u} ↥X
x : ↥X
mp : IsClosed (X := ↥X) {x} → LocallyOfFiniteType (X.fromSpecResidueField x)
mpr : LocallyOfFiniteType (X.fromSpecResidueField x) → IsClosed (X := ↥X) {x}
⊢ IsClosed (X := ↥X) {x} ↔ LocallyOfFiniteType (X.fromSpecResidueField x)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X : Scheme
inst : JacobsonSpace.{u} ↥X
x : ↥X
⊢ IsClosed (X := ↥X) {x} → LocallyOfFiniteType (X.fromSpecResidueField x)

Tactic:
fun H ↦ have := isClosed_singleton_iff_isClosedImmersion.mp H; inferInstance

Premises used: inferInstance, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X : Scheme
inst : JacobsonSpace.{u} ↥X
x : ↥X
⊢ IsClosed (X := ↥X) {x} → LocallyOfFiniteType (X.fromSpecResidueField x)

Tactic:
exact fun H ↦ have := isClosed_singleton_iff_isClosedImmersion.mp H; inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X : Scheme
inst : JacobsonSpace.{u} ↥X
x : ↥X
H : LocallyOfFiniteType (X.fromSpecResidueField x)
⊢ IsClosed (X := ↥X) {x}

Tactic:
simpa using (X.fromSpecResidueField x).closePoints_subset_preimage_closedPoints
      (IsLocalRing.isClosed_singleton_closedPoint _)

Premises used: AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, IsLocalRing.isClosed_singleton_closedPoint, AlgebraicGeometry.Scheme.fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
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
⊢ @LocallyOfFinitePresentation =
    affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
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
h₁ 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
⊢ LocallyOfFinitePresentation f ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f

Tactic:
rw [locallyOfFinitePresentation_iff, affineLocally_iff_forall_isAffineOpen]

Premises used: AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.locallyOfFinitePresentation_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ LocallyOfFinitePresentation f

Tactic:
HasRingHomProperty.of_isOpenImmersion
    RingHom.finitePresentation_holdsForLocalizationAway.containsIdentities

Premises used: RingHom.HoldsForLocalizationAway.containsIdentities, AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion, RingHom.finitePresentation_holdsForLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @LocallyOfFinitePresentation

Tactic:
HasRingHomProperty.stableUnderComposition RingHom.finitePresentation_stableUnderComposition

Premises used: RingHom.finitePresentation_stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ LocallyOfFinitePresentation (Spec.map f) ↔ (CommRingCat.Hom.hom f).FinitePresentation

Tactic:
HasRingHomProperty.Spec_iff

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : LocallyOfFinitePresentation f
⊢ (CommRingCat.Hom.hom (appTop f)).FinitePresentation

Tactic:
HasRingHomProperty.appTop (P := @LocallyOfFinitePresentation) _ inferInstance

Premises used: inferInstance, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyOfFinitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : LocallyOfFinitePresentation f
hg : LocallyOfFinitePresentation g
⊢ LocallyOfFinitePresentation (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @LocallyOfFinitePresentation

Tactic:
HasRingHomProperty.isStableUnderBaseChange RingHom.finitePresentation_isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange, RingHom.finitePresentation_isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : LocallyOfFinitePresentation g
⊢ LocallyOfFinitePresentation (X := Limits.pullback f g) (Limits.pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : LocallyOfFinitePresentation f
⊢ LocallyOfFinitePresentation (X := Limits.pullback f g) (Limits.pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : LocallyOfFinitePresentation f
⊢ LocallyOfFinitePresentation (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : LocallyOfFinitePresentation f
⊢ LocallyOfFinitePresentation (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation] at hf

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, AlgebraicGeometry.LocallyOfFinitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
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
rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
⊢ LocallyOfFiniteType f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType]

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, AlgebraicGeometry.LocallyOfFiniteType