awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  Eq (α := 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))))
    (Set.preimage (β := ↥Y) (⇑(pullback.snd f ι ≫ ι)) (singleton (α := ↥Y) ((pullback.snd f ι ≫ ι) x : ↥Y)))
⊢ Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))

Tactic:
rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]

Premises used: Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base, CategoryTheory.Limits.pullback.condition, TopCat.coe_comp
-- 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
⊢ Eq (α := 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))))
    (Set.preimage (β := ↥Y) (⇑(pullback.snd f ι ≫ ι)) (singleton (α := ↥Y) ((pullback.snd f ι ≫ ι) x : ↥Y)))

Tactic:
simp [← Set.image_singleton, Set.preimage_comp, Set.preimage_image_eq _ ι.injective]

Premises used: Set.image_singleton, Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.injective, Set.preimage_image_eq
-- 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
⊢ Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))

Tactic:
have H : pullback.snd f ι ⁻¹' {pullback.snd f ι x} =
        pullback.fst f ι ⁻¹' f ⁻¹' {f (pullback.fst f ι x)} := by
      rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]
      simp [← Set.image_singleton, Set.preimage_comp, Set.preimage_image_eq _ ι.injective]
-- 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
H :
  Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
⊢ Topology.IsOpenEmbedding (X :=
    (↑(Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
          (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))) :
      Type u))
    (Set.restrictPreimage (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))
      ⇑(pullback.fst f ι))

Tactic:
(f ⁻¹' {f (pullback.fst f ι x)}).restrictPreimage_isOpenEmbedding
          (pullback.fst f ι).isOpenEmbedding

Premises used: Set.restrictPreimage_isOpenEmbedding, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Set.preimage, CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.PresheafedSpace.Hom.base, Singleton.singleton, DFunLike.coe
-- 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
H :
  Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
a :
  Topology.IsOpenEmbedding f' ↔
    Topology.IsOpenEmbedding (X :=
      (↑(Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
            (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))) :
        Type u))
      (Set.restrictPreimage (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))
        ⇑(pullback.fst f ι))
⊢ Topology.IsOpenEmbedding f'

Tactic:
convert!
        (f ⁻¹' {f (pullback.fst f ι x)}).restrictPreimage_isOpenEmbedding
          (pullback.fst f ι).isOpenEmbedding using 0

Premises used: Set.restrictPreimage_isOpenEmbedding, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Set.preimage, CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.PresheafedSpace.Hom.base, Singleton.singleton, DFunLike.coe
-- 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
H :
  Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
⊢ Topology.IsOpenEmbedding (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))
      (Y := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u))
      (Set.MapsTo.restrict (⇑(pullback.fst f ι))
        (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
          (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
        (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯) ↔
    Topology.IsOpenEmbedding (X :=
      (↑(Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
            (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))) :
        Type u))
      (Set.MapsTo.restrict (⇑(pullback.fst f ι))
        (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
          (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
        (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯)

Tactic:
congr!
-- 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
H :
  Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
⊢ Topology.IsOpenEmbedding f'

Tactic:
have : Topology.IsOpenEmbedding f' := by
      convert!
        (f ⁻¹' {f (pullback.fst f ι x)}).restrictPreimage_isOpenEmbedding
          (pullback.fst f ι).isOpenEmbedding using 0
      dsimp [f', Set.restrictPreimage]
      congr!
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this_1 :
  ∀ {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
H :
  Eq (α := 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))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
this : Topology.IsOpenEmbedding f'
⊢ 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 })) ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u))
      {f'
          (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:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) 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 ⟨R, rfl⟩ := hY

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

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

Tactic:
obtain ⟨i, x, rfl⟩ := X.affineCover.exists_eq x

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

Tactic:
this (x := x) _ (f := ι ≫ f) ⟨_, rfl⟩

Premises used: Exists.intro, rfl