awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ @RingHom.comp _ (↑Γ(X, V) : Type u) _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(↑e :
              (↑(X.presheaf.stalk (↑⟨x, hxV⟩ : ↥X)) : Type u) →ₐ[(↑Γ(X, V) : Type u)]
                Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal) :
          (↑(X.presheaf.stalk (↑⟨x, hxV⟩ : ↥X)) : Type u) →+* Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
        (algebraMap (↑Γ(X, V) : Type u)
          (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V.carrier) x hxV) : ↥X)) : Type u)))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)) =
    (e.toRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))).comp
      (CommRingCat.Hom.hom (appLE f U V ⋯))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
x : ↥X
⊢ QuasiFiniteAt f x

Tactic:
HasRingHomProperty.stalkMap ?_ ‹_› x

Premises used: AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyQuasiFinite f
x : ↥X
refine :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    f.QuasiFinite →
      ∀ (J : Ideal S) (x : J.IsPrime),
        RingHom.QuasiFinite (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
⊢ QuasiFiniteAt f x

Tactic:
refine HasRingHomProperty.stalkMap ?_ ‹_› x

Premises used: AlgebraicGeometry.HasRingHomProperty.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
⊢ Algebra.QuasiFinite R S

Tactic:
algebraize [f]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
⊢ RingHom.QuasiFinite (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
    (Localization.localRingHom (Ideal.comap f J) J f ⋯)

Tactic:
.of_comp (g := algebraMap R _) ?_

Premises used: RingHom.QuasiFinite.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
refine :
  RingHom.QuasiFinite (S := Localization.AtPrime J)
    (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
      (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
⊢ RingHom.QuasiFinite (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
    (Localization.localRingHom (Ideal.comap f J) J f ⋯)

Tactic:
refine .of_comp (g := algebraMap R _) ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
⊢ RingHom.QuasiFinite (S := Localization.AtPrime J) (algebraMap R (Localization.AtPrime J))

Tactic:
RingHom.quasiFinite_algebraMap.mpr
      (inferInstance : Algebra.QuasiFinite R (Localization.AtPrime J))

Premises used: Iff.mpr, inferInstance, RingHom.quasiFinite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h_1 : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
h :
  Eq (α := R →+* Localization.AtPrime J)
    (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
      (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
    (algebraMap R (Localization.AtPrime J))
⊢ RingHom.QuasiFinite (S := Localization.AtPrime J)
    (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
      (algebraMap R (Localization.AtPrime (Ideal.comap f J))))

Tactic:
convert!
    RingHom.quasiFinite_algebraMap.mpr
      (inferInstance : Algebra.QuasiFinite R (Localization.AtPrime J))

Premises used: Iff.mpr, inferInstance, RingHom.quasiFinite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h_1 : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
h :
  ∀ (x : R),
    Eq (α := Localization.AtPrime J)
      ((RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
              (algebraMap R (Localization.AtPrime (Ideal.comap f J))) :
            (a : R) → Localization.AtPrime J)
          x :
        Localization.AtPrime J)
      ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
⊢ Eq (α := R →+* Localization.AtPrime J)
    (RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
      (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
    (algebraMap R (Localization.AtPrime J))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h_1 : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
x_1 : R
h :
  Eq (α := Localization.AtPrime J)
    ((algebraMap S (Localization.AtPrime J) : (a : S) → Localization.AtPrime J) ((f : (a : R) → S) x_1) :
      Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x_1 : Localization.AtPrime J)
⊢ Eq (α := Localization.AtPrime J)
    ((RingHom.comp (β := Localization.AtPrime (Ideal.comap f J)) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
            (algebraMap R (Localization.AtPrime (Ideal.comap f J))) :
          (a : R) → Localization.AtPrime J)
        x_1 :
      Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x_1 : Localization.AtPrime J)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f_1 : X ⟶ Y
inst : LocallyQuasiFinite f_1
x : ↥X
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
h : J.IsPrime
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.QuasiFinite R S
x_1 : R
⊢ Eq (α := Localization.AtPrime J)
    ((algebraMap S (Localization.AtPrime J) : (a : S) → Localization.AtPrime J) ((f : (a : R) → S) x_1) :
      Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x_1 : Localization.AtPrime J)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst : IsOpenImmersion f
⊢ QuasiFiniteAt (f ≫ g) x ↔ QuasiFiniteAt g (f x)

Tactic:
simp only [QuasiFiniteAt, stalkMap_comp, CommRingCat.hom_comp,
    RingHom.QuasiFinite.respectsIso.cancel_right_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt, RingHom.QuasiFinite.respectsIso, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst : LocallyQuasiFinite g
simp :
  (CommRingCat.Hom.hom (stalkMap g (f x) ≫ stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
⊢ QuasiFiniteAt (f ≫ g) x ↔ QuasiFiniteAt f x

Tactic:
simp only [QuasiFiniteAt, stalkMap_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst : LocallyQuasiFinite g
⊢ (CommRingCat.Hom.hom (stalkMap g (f x) ≫ stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite

Tactic:
RingHom.QuasiFinite.comp_iff (g.quasiFiniteAt _)

Premises used: RingHom.QuasiFinite.comp_iff, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst : LocallyQuasiFinite g
⊢ (CommRingCat.Hom.hom (stalkMap g (f x) ≫ stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite

Tactic:
exact RingHom.QuasiFinite.comp_iff (g.quasiFiniteAt _)

Premises used: RingHom.QuasiFinite.comp_iff, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
rw : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x))
rw₁ : QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x))
rw₂ : QuasiFiniteAt f x ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
rw₃ rw₄ : (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (X.fromSpecStalk x ≫ f)

Tactic:
rw [← SpecMap_stalkMap_fromSpecStalk, LocallyQuasiFinite.comp_iff,
    HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), QuasiFiniteAt]

Premises used: AlgebraicGeometry.LocallyQuasiFinite.comp_iff, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt, AlgebraicGeometry.HasRingHomProperty.Spec_iff, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
rw :
  QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      (Set.image (α := ↥(fiber f (f x))) (⇑(fiberHomeo f (f x)) : (a : ↥(fiber f (f x))) → (↑(⇑f ⁻¹' {f x}) : Type u))
        {asFiber f x})
⊢ QuasiFiniteAt f x ↔ IsOpen (X := ↥(fiber f (f x))) {asFiber f x}

Tactic:
rw [← (f.fiberHomeo (f x)).isOpen_image]

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.fiberHomeo, AlgebraicGeometry.PresheafedSpace.Hom.base, Homeomorph.isOpen_image, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
simp :
  QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      (Set.image (α := ↥(fiber f (f x))) (⇑(fiberHomeo f (f x)) : (a : ↥(fiber f (f x))) → (↑(⇑f ⁻¹' {f x}) : Type u))
        {asFiber f x})

Tactic:
simp only [Set.image_singleton, asFiber, Homeomorph.apply_symm_apply]

Premises used: Set.image_singleton, AlgebraicGeometry.Scheme.Hom.asFiber, Homeomorph.apply_symm_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        QuasiFiniteAt f x ↔
          IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
            {Subtype.mk (p := fun (x_1 : ↥X) ↦
                Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯})
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
wlog :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.I₀) (y : ↥(Y.affineCover.X i)) (hy : Eq (α := ↥Y) ((Y.affineCover.f i) y : ↥Y) (f x : ↥Y)),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}

Tactic:
obtain ⟨i, y, hy⟩ := Y.affineCover.exists_eq (f x)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
y : ↥(Y.affineCover.X i)
hy : Eq (α := ↥Y) ((Y.affineCover.f i) y : ↥Y) (f x : ↥Y)
inr :
  ∀ (x : ↥(pullback f (Y.affineCover.f i)))
    (hy :
      Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
        (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)),
    QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔
      IsOpen (X :=
        (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
          Type u))
        (singleton (α :=
          (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
            Type u))
          (Subtype.mk (p := fun (x_1 : ↥X) ↦
              Membership.mem (γ := Set ↥X)
                (Set.preimage (β := ↥Y) (⇑f)
                  (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
                x_1)
              ((pullback.fst f (Y.affineCover.f i)) x) ⋯ :
            { x_1 : ↥X //
              Membership.mem (γ := Set ↥X)
                (Set.preimage (β := ↥Y) (⇑f)
                  (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
                x_1 }))
⊢ QuasiFiniteAt f x ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}

Tactic:
obtain ⟨x, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback _ _ hy.symm

Premises used: Eq.symm, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy :
  Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
    (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ QuasiFiniteAt (pullback.snd f ι) x ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
            (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
        Type u))
      {Subtype.mk (p := fun (x_1 : ↥(pullback f ι)) ↦
          Membership.mem (γ := Set ↥(pullback f ι))
            (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
              (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
            x_1)
          x ⋯}

Tactic:
this (f := pullback.snd f ι) (x := x) ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy :
  Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
    (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ QuasiFiniteAt (pullback.snd f ι) x

Tactic:
(RingHom.QuasiFinite.respectsIso.arrow_mk_iso_iff
        (Scheme.stalkMapIsoOfIsPullback (.of_hasPullback f ι) x))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.stalkMapIsoOfIsPullback, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt, RingHom.QuasiFinite.respectsIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy :
  Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
    (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ QuasiFiniteAt (pullback.snd f ι) x

Tactic:
exact (RingHom.QuasiFinite.respectsIso.arrow_mk_iso_iff
        (Scheme.stalkMapIsoOfIsPullback (.of_hasPullback f ι) x))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.stalkMapIsoOfIsPullback, RingHom.QuasiFinite.respectsIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, RingHom.RespectsIso.arrow_mk_iso_iff