awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal R
inst_7 : p.IsPrime
P : Ideal S
inst_8 : P.IsPrime
inst_9 : P.LiesOver p
inst_10 : QuasiFiniteAt R P
inst_11 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime P)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p P
m : Ideal (Localization.AtPrime P) := IsLocalRing.maximalIdeal (Localization.AtPrime P)
this_1 : m.LiesOver p := ⋯
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime m) :=
  Localization.AtPrime.algebraOfLiesOver p m
this : Algebra (Localization.AtPrime P) (Localization.AtPrime m) := Localization.AtPrime.algebraOfLiesOver P m
e : AlgEquiv.{u_1, u_2, u_2} p.ResidueField P.ResidueField m.ResidueField :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom p.ResidueField P.ResidueField m.ResidueField) ⋯
⊢ Module.Finite.{u_1, u_2} p.ResidueField P.ResidueField

Tactic:
.of_surjective e.symm.toLinearMap e.symm.surjective

Premises used: Module.Finite.of_surjective, AlgEquiv.symm, AlgEquiv.toLinearMap, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal R
inst_7 : p.IsPrime
P : Ideal S
inst_8 : P.IsPrime
inst_9 : P.LiesOver p
inst_10 : QuasiFiniteAt R P
inst_11 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime P)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p P
m : Ideal (Localization.AtPrime P) := IsLocalRing.maximalIdeal (Localization.AtPrime P)
this_1 : m.LiesOver p := ⋯
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime m) :=
  Localization.AtPrime.algebraOfLiesOver p m
this : Algebra (Localization.AtPrime P) (Localization.AtPrime m) := Localization.AtPrime.algebraOfLiesOver P m
e : AlgEquiv.{u_1, u_2, u_2} p.ResidueField P.ResidueField m.ResidueField :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom p.ResidueField P.ResidueField m.ResidueField) ⋯
⊢ Module.Finite.{u_1, u_2} p.ResidueField P.ResidueField

Tactic:
exact .of_surjective e.symm.toLinearMap e.symm.surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
y : Localization.AtPrime p
⊢ HSMul.hSMul (α := ↥p.primeCompl) (y, 1).2 y =
    (LinearMap.id : (a : Localization.AtPrime p) → Localization.AtPrime p) (y, 1).1

Tactic:
simp
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
⊢ ∀ {x₁ x₂ : Localization.AtPrime p},
    Eq (α := Localization.AtPrime p)
        ((LinearMap.id : (a : Localization.AtPrime p) → Localization.AtPrime p) x₁ : Localization.AtPrime p)
        ((LinearMap.id : (a : Localization.AtPrime p) → Localization.AtPrime p) x₂ : Localization.AtPrime p) →
      ∃ (c : ↥p.primeCompl), c • x₁ = c • x₂

Tactic:
simpa using ⟨1, p.primeCompl.one_mem⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
⊢ IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id

Tactic:
have : IsLocalizedModule p.primeCompl (.id (R := S) (M := Localization.AtPrime p)) :=
    ⟨IsLocalizedModule.map_units (Algebra.linearMap S (Localization.AtPrime p)),
      fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, p.primeCompl.one_mem⟩⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
⊢ Module.Finite.{u_1, u_2} R (Localization.AtPrime p)

Tactic:
have : Module.Finite R (Localization.AtPrime p) := .of_quasiFinite
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
⊢ Module.Finite S (Localization.AtPrime p)

Tactic:
have : Module.Finite S (Localization.AtPrime p) := .of_restrictScalars_finite R _ _
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this : Module.Finite S (Localization.AtPrime p)
⊢ IsArtinianRing.{u_2} (Localization.AtPrime p)

Tactic:
have : IsArtinianRing (Localization.AtPrime p) := .of_finite R _
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this : IsArtinianRing.{u_2} (Localization.AtPrime p)
⊢ IsNoetherianRing S

Tactic:
have : IsNoetherianRing S := Algebra.EssFiniteType.isNoetherianRing R S
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this : IsNoetherianRing S
⊢ Module.FinitePresentation S (Localization.AtPrime p)

Tactic:
have : Module.FinitePresentation S (Localization.AtPrime p) :=
    Module.finitePresentation_of_finite _ _
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this : Module.FinitePresentation S (Localization.AtPrime p)
obtain :
  ∀ (r : S) (hrp : r ∈ p.primeCompl)
    (H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))),
    ∃ f ∉ p,
      (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}

Tactic:
obtain ⟨r, hrp, H⟩ := IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation
    p.primeCompl (Algebra.linearMap S (Localization.AtPrime p))

Premises used: Localization.AtPrime, Algebra.linearMap, IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation, Ideal.primeCompl
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
⊢ IsLocalization (Submonoid.powers r) (Localization.AtPrime p)

Tactic:
have : IsLocalization (.powers r) (Localization.AtPrime p) :=
    (isLocalizedModule_iff_isLocalization' _ _).mp H
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}

Tactic:
⟨r, hrp, subset_antisymm (fun q hrq ↦ ?_) (Set.singleton_subset_iff.mpr hrp)⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, subset_antisymm, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
refine :
  ∀ (q : PrimeSpectrum S) (hrq : q ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))),
    Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }} q
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}

Tactic:
refine ⟨r, hrp, subset_antisymm (fun q hrq ↦ ?_) (Set.singleton_subset_iff.mpr hrp)⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
q : PrimeSpectrum S
hrq : q ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))
obtain :
  ∀ (q : PrimeSpectrum (Localization.Away r))
    (hrq :
      PrimeSpectrum.comap (algebraMap S (Localization.Away r)) q ∈
        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))),
    Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
      (PrimeSpectrum.comap (algebraMap S (Localization.Away r)) q)
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }} q

Tactic:
obtain ⟨q, rfl⟩ := (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r).ge hrq

Premises used: Eq.ge, Localization.Away, PrimeSpectrum.localization_away_comap_range, rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
q : PrimeSpectrum (Localization.Away r)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r)) q ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))
obtain :
  ∀ (q : PrimeSpectrum (Localization.AtPrime p))
    (hrq :
      PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
          (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
              (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
            q) ∈
        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))),
    Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
      (PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
        (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
            (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
          q))
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
    (PrimeSpectrum.comap (algebraMap S (Localization.Away r)) q)

Tactic:
obtain ⟨q, rfl⟩ := (PrimeSpectrum.comapEquiv φ.toRingEquiv).symm.surjective q

Premises used: PrimeSpectrum.comapEquiv, OrderIso.surjective, OrderIso.symm, AlgEquiv.toRingEquiv, rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
q : PrimeSpectrum (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
      (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
          (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
        q) ∈
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))
⊢ q = IsLocalRing.closedPoint (Localization.AtPrime p)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
q : PrimeSpectrum (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
      (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
          (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
        q) ∈
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))
obtain :
  ∀
    (hrq :
      PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
          (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
              (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
            (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))),
    Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
      (PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
        (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
            (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
          (IsLocalRing.closedPoint (Localization.AtPrime p))))
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
    (PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
      (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
          (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
        q))

Tactic:
obtain rfl : q = IsLocalRing.closedPoint _ := Subsingleton.elim _ _

Premises used: IsLocalRing.closedPoint, Subsingleton.elim, rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
      (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
          (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
        (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))
asIdeal :
  PrimeSpectrum.asIdeal
      (PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
        (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
            (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
          (IsLocalRing.closedPoint (Localization.AtPrime p)))) =
    { asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
    (PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
      (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
          (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
        (IsLocalRing.closedPoint (Localization.AtPrime p))))

Tactic:
ext1
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this_5 : IsNoetherianRing S
this_6 : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away (M' := Localization.AtPrime p) r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
      (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
          (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
        (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum S))
asIdeal :
  Ideal.comap (F := S →+* Localization.Away r) (algebraMap S (Localization.Away r))
      (Ideal.comap (F := Localization.Away r →+* Localization.AtPrime p)
        (↑φ : Localization.Away r →+* Localization.AtPrime p)
        (PrimeSpectrum.asIdeal (IsLocalRing.closedPoint (Localization.AtPrime p)))) =
    p
⊢ PrimeSpectrum.asIdeal
      (PrimeSpectrum.comap (S := Localization.Away r) (algebraMap S (Localization.Away r))
        (((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm :
            (a : PrimeSpectrum (Localization.AtPrime p)) → PrimeSpectrum (Localization.Away r))
          (IsLocalRing.closedPoint (Localization.AtPrime p)))) =
    { asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }.asIdeal

Tactic:
dsimp [-RingEquiv.symm_mk]

Premises used: RingEquiv.symm_mk