awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
⊢ ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))

Tactic:
ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective _
    (.of_finiteType_of_weaklyQuasiFiniteAt _)

Premises used: Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H : ZariskisMainProperty R p
obtain :
  ∀ (S' : Subalgebra R S)
    (hS' :
      Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S'))
    (r : ↥S') (hrp : (↑r : S) ∉ p)
    (H :
      Function.Bijective (α := Localization.Away r) (β :=
        Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
        (⇑(Localization.awayMap S'.val.toRingHom r) :
          (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))),
    QuasiFiniteAt R p
⊢ QuasiFiniteAt R p

Tactic:
obtain ⟨S', hS', r, hrp, H⟩ := H.exists_fg_and_exists_notMem_and_awayMap_bijective _

Premises used: Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
⊢ Module.Finite.{u_1, u_2} R ↥S'

Tactic:
have : Module.Finite R S' := ⟨(Submodule.fg_top _).mpr hS'⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this : Module.Finite.{u_1, u_2} R ↥S'
⊢ QuasiFinite.{u_1, u_2} R (Localization.Away r)

Tactic:
have : Algebra.QuasiFinite R (Localization.Away r) :=
    .trans _ S' _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this : QuasiFinite.{u_1, u_2} R (Localization.Away r)
⊢ QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))

Tactic:
have : Algebra.QuasiFinite R (Localization.Away r.1) :=
    .of_surjective_algHom (Localization.awayMapₐ S'.val r) H.2
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
⊢ ∀ (y : ↥(Submonoid.powers (↑r : S))),
    IsUnit (M := Localization.AtPrime p)
      ((ofId S (Localization.AtPrime p) : (a : S) → Localization.AtPrime p) (↑y : S) : Localization.AtPrime p)

Tactic:
simpa [Submonoid.mem_powers_iff] using
        (IsLocalization.map_units (M := p.primeCompl) (Localization.AtPrime p) ⟨r, hrp⟩).pow

Premises used: Localization.AtPrime, IsUnit.pow, Subtype.mk, IsLocalization.map_units, Submonoid.mem_powers_iff, Subtype.val
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
⊢ QuasiFiniteAt R p

Tactic:
.of_forall_exists_mul_mem_range (f.restrictScalars R) fun x ↦ ?_

Premises used: AlgHom.restrictScalars, Algebra.QuasiFinite.of_forall_exists_mul_mem_range
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
refine :
  ∀ (x : Localization.AtPrime p),
    ∃ (s : Localization.Away (↑r : S)),
      IsUnit (M := Localization.AtPrime p)
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
            Localization.AtPrime p) ∧
        Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
          (HMul.hMul (β := Localization.AtPrime p) x
            ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
              Localization.AtPrime p))
⊢ QuasiFiniteAt R p

Tactic:
refine .of_forall_exists_mul_mem_range (f.restrictScalars R) fun x ↦ ?_
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
x : Localization.AtPrime p
obtain :
  ∀ (x s : S) (hs : s ∈ p.primeCompl),
    ∃ (s_1 : Localization.Away (↑r : S)),
      IsUnit (M := Localization.AtPrime p)
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s_1 :
            Localization.AtPrime p) ∧
        Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
          (HMul.hMul (α := Localization.AtPrime p) (β := Localization.AtPrime p)
            (IsLocalization.mk' (Localization.AtPrime p) x (Subtype.mk (p := fun (x : S) ↦ x ∈ p.primeCompl) s hs) :
              Localization.AtPrime p)
            ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s_1 :
              Localization.AtPrime p))
⊢ ∃ (s : Localization.Away (↑r : S)),
    IsUnit (M := Localization.AtPrime p)
        ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
          Localization.AtPrime p) ∧
      Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
        (HMul.hMul (β := Localization.AtPrime p) x
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
            Localization.AtPrime p))

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ IsUnit (M := Localization.AtPrime p)
    ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p)
        ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) s) :
      Localization.AtPrime p)

Tactic:
simpa using IsLocalization.map_units _ ⟨s, hs⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ (AlgHom.toRingHom (AlgHom.restrictScalars R f) : (a : Localization.Away (↑r : S)) → Localization.AtPrime p)
      ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) x) =
    HMul.hMul (α := Localization.AtPrime p) (β := Localization.AtPrime p)
      (IsLocalization.mk' (Localization.AtPrime p) x (Subtype.mk (p := fun (x : S) ↦ x ∈ p.primeCompl) s hs) :
        Localization.AtPrime p)
      ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p)
          ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) s) :
        Localization.AtPrime p)

Tactic:
simp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ ∃ (s_1 : Localization.Away (↑r : S)),
    IsUnit (M := Localization.AtPrime p)
        ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s_1 :
          Localization.AtPrime p) ∧
      Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
        (HMul.hMul (α := Localization.AtPrime p) (β := Localization.AtPrime p)
          (IsLocalization.mk' (Localization.AtPrime p) x (Subtype.mk (p := fun (x : S) ↦ x ∈ p.primeCompl) s hs) :
            Localization.AtPrime p)
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s_1 :
            Localization.AtPrime p))

Tactic:
exact ⟨algebraMap _ _ s, by simpa using IsLocalization.map_units _ ⟨s, hs⟩,
    algebraMap _ _ x, by simp⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
⊢ QuasiFiniteAt R p

Tactic:
ZariskisMainProperty.quasiFiniteAt _ (.of_finiteType_of_weaklyQuasiFiniteAt _)

Premises used: Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt, Algebra.ZariskisMainProperty.quasiFiniteAt
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
q : Ideal S
inst_4 : q.IsPrime
inst_5 : p.IsPrime
inst_6 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_7 : Q.IsPrime
hQ : Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_8 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
⊢ QuasiFiniteAt R q

Tactic:
have : Algebra.WeaklyQuasiFiniteAt R q := .of_quasiFiniteAt_residueField p q Q hQ
  .of_weaklyQuasiFiniteAt _

Premises used: Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt, Algebra.WeaklyQuasiFiniteAt.of_quasiFiniteAt_residueField
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H :
  IsOpen (X :=
    (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {PrimeSpectrum.comap (algebraMap R S) q}) :
      Type u_2))
    {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q})
          x)
        q ⋯}
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
suffices :
  QuasiFiniteAt p.asIdeal.ResidueField (S := p.asIdeal.Fiber S)
    (PrimeSpectrum.asIdeal
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯)))
⊢ QuasiFiniteAt R q.asIdeal

Tactic:
suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    .of_quasiFiniteAt_residueField _ q.asIdeal (e ⟨q, rfl⟩).asIdeal
      congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H :
  IsOpen (X :=
    (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {PrimeSpectrum.comap (algebraMap R S) q}) :
      Type u_2))
    {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q})
          x)
        q ⋯}
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ QuasiFiniteAt p.asIdeal.ResidueField (S := p.asIdeal.Fiber S)
    (PrimeSpectrum.asIdeal
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯)))

Tactic:
.of_isOpen_singleton _ ?_

Premises used: Algebra.QuasiFiniteAt.of_isOpen_singleton
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H :
  IsOpen (X :=
    (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {PrimeSpectrum.comap (algebraMap R S) q}) :
      Type u_2))
    {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q})
          x)
        q ⋯}
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
refine :
  IsOpen (X := PrimeSpectrum (p.asIdeal.Fiber S))
    (singleton (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
            Membership.mem (γ := Set (PrimeSpectrum S))
              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
            q ⋯) :
        PrimeSpectrum (p.asIdeal.Fiber S)))
⊢ QuasiFiniteAt p.asIdeal.ResidueField (S := p.asIdeal.Fiber S)
    (PrimeSpectrum.asIdeal
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯)))

Tactic:
refine .of_isOpen_singleton _ ?_
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H :
  IsOpen (X :=
    (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {PrimeSpectrum.comap (algebraMap R S) q}) :
      Type u_2))
    {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q})
          x)
        q ⋯}
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
rwa :
  IsOpen (X := PrimeSpectrum (p.asIdeal.Fiber S))
    (Set.image (α :=
      { x : PrimeSpectrum S //
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x })
      (⇑e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
      {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯})
rwa₁ rwa₂ rwa₃ rwa₄ :
  IsOpen (X := (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2))
    {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
        q ⋯}
⊢ IsOpen (X := PrimeSpectrum (p.asIdeal.Fiber S))
    (singleton (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
            Membership.mem (γ := Set (PrimeSpectrum S))
              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
            q ⋯) :
        PrimeSpectrum (p.asIdeal.Fiber S)))

Tactic:
rwa [← Set.image_singleton, e.isOpen_image]

Premises used: Set.image_singleton, Homeomorph.isOpen_image