awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
⊢ Set.Finite (α := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))

Tactic:
(hf (Y.affineCover.f i x)).preimage
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective.injOn

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, CategoryTheory.ConcreteCategory.hom, Function.Injective.injOn, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Set.Finite.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
h :
  Eq (α := Set ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
    (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
⊢ Set.Finite (α := ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})

Tactic:
convert!
      (hf (Y.affineCover.f i x)).preimage
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective.injOn

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, CategoryTheory.ConcreteCategory.hom, Function.Injective.injOn, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Set.Finite.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
h :
  ∀ (x_1 : ↥(pullback f (Y.affineCover.f i))),
    Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
        (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x}) x_1 ↔
      Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
        (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
          (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
        x_1
⊢ Eq (α := Set ↥(pullback f (Y.affineCover.f i)))
    (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x})
    (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    id (LocallyQuasiFinite f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
x_1 : ↥(pullback f (Y.affineCover.f i))
⊢ Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
      (Set.preimage (β := ↥(Y.affineCover.X i)) ⇑(pullback.snd f (Y.affineCover.f i)) {x}) x_1 ↔
    Membership.mem (γ := Set ↥(pullback f (Y.affineCover.f i)))
      (Set.preimage (β := ↥X) (⇑(pullback.fst f (Y.affineCover.f i)))
        (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) ((Y.affineCover.f i) x : ↥Y))))
      x_1

Tactic:
simp [← (Y.affineCover.f i).isOpenEmbedding.injective.eq_iff, ← Scheme.Hom.comp_apply,
      -Hom.comp_base, pullback.condition]

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, Function.Injective.eq_iff, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, AlgebraicGeometry.Scheme.Hom.comp_base, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})), id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
        (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
wlog :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ id (LocallyQuasiFinite f)

Tactic:
(IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ _
      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn :)) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, Function.Injective.injOn, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Topology.IsEmbedding.injective, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl, Set.Finite.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x}))
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), id (LocallyQuasiFinite f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ id (LocallyQuasiFinite f)

Tactic:
exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ _
      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn :)) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, Function.Injective.injOn, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Topology.IsEmbedding.injective, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl, Set.Finite.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥X) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f]
    (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑f {x})),
    id (LocallyQuasiFinite f)
⊢ id (LocallyQuasiFinite f)

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑f {x})
obtain :
  ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)]
    (hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})),
    id (LocallyQuasiFinite (Spec.map φ))
⊢ id (LocallyQuasiFinite f)

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFiniteType (Spec.map φ)
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
simp : (CommRingCat.Hom.hom φ).FiniteType → (CommRingCat.Hom.hom φ).QuasiFinite
⊢ id (LocallyQuasiFinite (Spec.map φ))

Tactic:
simp only [HasRingHomProperty.Spec_iff, id_eq] at *

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff, id_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
inst : (CommRingCat.Hom.hom φ).FiniteType
⊢ Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
inst : (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)
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
(Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr hf

Premises used: Iff.mpr, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, RingHom.QuasiFinite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), Set.Finite (α := ↥(Spec S)) (Set.preimage (β := ↥(Spec R)) ⇑(Spec.map φ) {x})
inst : (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)
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
exact (Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr hf

Premises used: Iff.mpr, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : QuasiCompact f
⊢ LocallyQuasiFinite f ↔ ∀ (x : ↥Y), Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {x})

Tactic:
⟨fun _ ↦ f.finite_preimage_singleton, .of_finite_preimage_singleton f⟩

Premises used: Iff.intro, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, AlgebraicGeometry.LocallyQuasiFinite.of_finite_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ LocallyQuasiFinite f

Tactic:
.of_finite_preimage_singleton _ fun _ ↦ (Set.subsingleton_singleton.preimage hf).finite

Premises used: Set.subsingleton_singleton, AlgebraicGeometry.LocallyQuasiFinite.of_finite_preimage_singleton, Set.Subsingleton.finite, Set.Subsingleton.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : UniversallyInjective f
⊢ LocallyQuasiFinite f

Tactic:
.of_injective f.injective

Premises used: AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.LocallyQuasiFinite.of_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑(Y.presheaf.obj (Opposite.op U)) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
⊢ IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal

Tactic:
have := hU.isLocalization_stalk ⟨f x, (hVU hxV)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑(Y.presheaf.obj (Opposite.op U)) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
this :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
⊢ Algebra.QuasiFinite.{u, u} (↑(Y.presheaf.obj (Opposite.op U)) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u)

Tactic:
.of_isLocalization (hU.primeIdealOf ⟨_, hVU hxV⟩).asIdeal.primeCompl

Premises used: Algebra.QuasiFinite.of_isLocalization, Subtype.mk, AlgebraicGeometry.IsAffineOpen.primeIdealOf, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑(Y.presheaf.obj (Opposite.op U)) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
this :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
⊢ Algebra.QuasiFinite.{u, u} (↑(Y.presheaf.obj (Opposite.op U)) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u)

Tactic:
exact .of_isLocalization (hU.primeIdealOf ⟨_, hVU hxV⟩).asIdeal.primeCompl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
⊢ RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))

Tactic:
have H : (Y.presheaf.germ U _ (hVU hxV)).hom.QuasiFinite := by
    algebraize [(Y.presheaf.germ U _ (hVU hxV)).hom]
    have := hU.isLocalization_stalk ⟨f x, (hVU hxV)⟩
    rw [← (Y.presheaf.germ U _ (hVU hxV)).hom.algebraMap_toAlgebra,
      RingHom.quasiFinite_algebraMap]
    exact .of_isLocalization (hU.primeIdealOf ⟨_, hVU hxV⟩).asIdeal.primeCompl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal

Tactic:
have := hV.isLocalization_stalk ⟨x, hxV⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
e : (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) :
    Type u) ≃ₐ[(↑Γ(X, V) : Type u)]
  Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal.primeCompl
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
rw :
  RingHom.QuasiFinite.{u, u} (R := (↑Γ(Y, U) : Type u)) (S :=
    Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
    (algebraMap (↑Γ(Y, U) : Type u)
      (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal))
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal

Tactic:
rw [RingHom.QuasiFiniteAt, Algebra.QuasiFiniteAt, ← RingHom.quasiFinite_algebraMap]

Premises used: RingHom.QuasiFiniteAt, Algebra.QuasiFiniteAt, RingHom.quasiFinite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
e : (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) :
    Type u) ≃ₐ[(↑Γ(X, V) : Type u)]
  Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal.primeCompl
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
⊢ (e.toRingEquiv.toRingHom.comp
      ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)))).QuasiFinite

Tactic:
(RingHom.QuasiFinite.of_finite e.finite).comp (hx.comp H)

Premises used: RingEquiv.finite, AlgEquiv.toRingEquiv, RingHom.QuasiFinite.comp, RingHom.QuasiFinite.of_finite
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : RingHom.QuasiFinite (S := (↑(Y.presheaf.stalk (f x)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯))
algInst_1 : Algebra (↑(X.presheaf.obj (Opposite.op V)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
e : (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) :
    Type u) ≃ₐ[(↑Γ(X, V) : Type u)]
  Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal.primeCompl
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) : Type u)
    (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
h :
  algebraMap (↑Γ(Y, U) : Type u)
      (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal) =
    e.toRingEquiv.toRingHom.comp
      ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)))
⊢ RingHom.QuasiFinite.{u, u} (R := (↑Γ(Y, U) : Type u)) (S :=
    Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal)
    (algebraMap (↑Γ(Y, U) : Type u)
      (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal))

Tactic:
convert! (RingHom.QuasiFinite.of_finite e.finite).comp (hx.comp H)

Premises used: RingEquiv.finite, AlgEquiv.toRingEquiv, RingHom.QuasiFinite.comp, RingHom.QuasiFinite.of_finite