awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.AtPrime p) (algebraMap S (Localization.AtPrime p))
      (PrimeSpectrum.asIdeal (IsLocalRing.closedPoint (Localization.AtPrime p))) =
    p
⊢ 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

Tactic:
rw [Ideal.comap_comap, ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap, Ideal.comap_comap
-- 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))
⊢ Ideal.comap (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p))
      (PrimeSpectrum.asIdeal (IsLocalRing.closedPoint (Localization.AtPrime p))) =
    p

Tactic:
IsLocalization.AtPrime.under_maximalIdeal _ _

Premises used: IsLocalRing.maximalIdeal, IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal
-- 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))
⊢ Ideal.comap (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p))
      (PrimeSpectrum.asIdeal (IsLocalRing.closedPoint (Localization.AtPrime p))) =
    p

Tactic:
exact IsLocalization.AtPrime.under_maximalIdeal _ _

Premises used: IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal
-- 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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
⊢ IsJacobsonRing S

Tactic:
have : IsJacobsonRing S := isJacobsonRing_of_finiteType (A := 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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
this : IsJacobsonRing S
⊢ IsNoetherianRing S

Tactic:
have : IsNoetherianRing S := Algebra.FiniteType.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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
this_1 : IsJacobsonRing S
this : IsNoetherianRing S
⊢ IsClopen (X := PrimeSpectrum S) {p}

Tactic:
((PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out 0 1).mp ?_

Premises used: List.TFAE.out, Iff.mp, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, OfNat.ofNat
-- 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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
this_1 : IsJacobsonRing S
this : IsNoetherianRing S
refine : IsOpen (X := PrimeSpectrum S) {p}
⊢ IsClopen (X := PrimeSpectrum S) {p}

Tactic:
refine ((PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out 0 1).mp ?_

Premises used: List.TFAE.out, Iff.mp, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, OfNat.ofNat
-- 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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
this_1 : IsJacobsonRing S
this : IsNoetherianRing S
obtain :
  ∀ (f : S) (hf : f ∉ p.asIdeal)
    (e :
      (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) =
        {{ asIdeal := p.asIdeal, isPrime := ⋯ : PrimeSpectrum S }}),
    IsOpen (X := PrimeSpectrum S) {p}
⊢ IsOpen (X := PrimeSpectrum S) {p}

Tactic:
obtain ⟨f, hf, e⟩ := exists_basicOpen_eq_singleton (R := R) p.asIdeal

Premises used: Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, PrimeSpectrum.asIdeal
-- 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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
this_1 : IsJacobsonRing S
this : IsNoetherianRing S
f : S
hf : f ∉ p.asIdeal
e : (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p.asIdeal, isPrime := ⋯ : PrimeSpectrum S }}
⊢ IsOpen (X := PrimeSpectrum S) {p}

Tactic:
e ▸ (PrimeSpectrum.basicOpen f).isOpen

Premises used: PrimeSpectrum.basicOpen, Eq.rec, TopologicalSpace.Opens.isOpen
-- 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 : PrimeSpectrum S
inst_3 : IsArtinianRing R
inst_4 : FiniteType R S
inst_5 : QuasiFiniteAt R p.asIdeal
this_1 : IsJacobsonRing S
this : IsNoetherianRing S
f : S
hf : f ∉ p.asIdeal
e : (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p.asIdeal, isPrime := ⋯ : PrimeSpectrum S }}
⊢ IsOpen (X := PrimeSpectrum S) {p}

Tactic:
exact e ▸ (PrimeSpectrum.basicOpen f).isOpen
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H : IsOpen (X := PrimeSpectrum S) {p}
⊢ IsNoetherianRing S

Tactic:
have : IsNoetherianRing S := Algebra.FiniteType.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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H : IsOpen (X := PrimeSpectrum S) {p}
this : IsNoetherianRing S
⊢ IsJacobsonRing S

Tactic:
have : IsJacobsonRing S := isJacobsonRing_of_finiteType (A := 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H : IsOpen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
⊢ IsClopen (X := PrimeSpectrum S) {p}

Tactic:
rw [(PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out
    0 1 rfl rfl] at H

Premises used: List.TFAE.out, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, OfNat.ofNat, 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H : IsOpen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
H₁ : IsClopen (X := PrimeSpectrum S) {p}
⊢ IsNoetherianRing S

Tactic:
rw [(PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out
    0 1 rfl rfl] at H

Premises used: List.TFAE.out, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, OfNat.ofNat, 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H : IsOpen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
H₁ : IsClopen (X := PrimeSpectrum S) {p}
this₁ : IsNoetherianRing S
⊢ IsJacobsonRing S

Tactic:
rw [(PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out
    0 1 rfl rfl] at H

Premises used: List.TFAE.out, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, OfNat.ofNat, 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
obtain :
  ∀ (e : S) (he : IsIdempotentElem e) (H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))),
    QuasiFiniteAt R p.asIdeal
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
obtain ⟨e, he, H⟩ := PrimeSpectrum.isClopen_iff.mp H

Premises used: PrimeSpectrum.isClopen_iff, Iff.mp
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
⊢ e ∉ p.asIdeal

Tactic:
have hep : e ∉ p.asIdeal := H.le 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
simp :
  ∀ (a : S) (b : Membership.mem (γ := Submonoid S) (Submonoid.powers e) a),
    IsUnit (M := Localization.AtPrime p.asIdeal)
      ((ofId S (Localization.AtPrime p.asIdeal) : (a : S) → Localization.AtPrime p.asIdeal) a :
        Localization.AtPrime p.asIdeal)
⊢ ∀ (y : ↥(Submonoid.powers e)),
    IsUnit (M := Localization.AtPrime p.asIdeal)
      ((ofId S (Localization.AtPrime p.asIdeal) : (a : S) → Localization.AtPrime p.asIdeal) (↑y : S) :
        Localization.AtPrime p.asIdeal)

Tactic:
simp only [Subtype.forall]

Premises used: Subtype.forall
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
⊢ ∀ (a : S) (b : Membership.mem (γ := Submonoid S) (Submonoid.powers e) a),
    IsUnit (M := Localization.AtPrime p.asIdeal)
      ((ofId S (Localization.AtPrime p.asIdeal) : (a : S) → Localization.AtPrime p.asIdeal) a :
        Localization.AtPrime p.asIdeal)

Tactic:
Submonoid.powers_le (P := (IsUnit.submonoid _).comap _).mpr ?_

Premises used: Iff.mpr, Set.Mem, setOf, IsUnit, Set.preimage, Submonoid.powers_le
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
refine :
  Membership.mem (γ := Submonoid S)
    (Submonoid.comap (F := S →ₐ[S] Localization.AtPrime p.asIdeal) (ofId S (Localization.AtPrime p.asIdeal))
      (IsUnit.submonoid (Localization.AtPrime p.asIdeal)))
    e
⊢ ∀ (a : S) (b : Membership.mem (γ := Submonoid S) (Submonoid.powers e) a),
    IsUnit (M := Localization.AtPrime p.asIdeal)
      ((ofId S (Localization.AtPrime p.asIdeal) : (a : S) → Localization.AtPrime p.asIdeal) a :
        Localization.AtPrime p.asIdeal)

Tactic:
refine Submonoid.powers_le (P := (IsUnit.submonoid _).comap _).mpr ?_

Premises used: Iff.mpr, Submonoid.powers_le
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
⊢ Membership.mem (γ := Submonoid S)
    (Submonoid.comap (F := S →ₐ[S] Localization.AtPrime p.asIdeal) (ofId S (Localization.AtPrime p.asIdeal))
      (IsUnit.submonoid (Localization.AtPrime p.asIdeal)))
    e

Tactic:
simpa [IsUnit.mem_submonoid_iff] using IsLocalization.map_units
        (M := p.asIdeal.primeCompl) _ ⟨e, hep⟩

Premises used: IsUnit.mem_submonoid_iff, Subtype.mk, IsLocalization.map_units
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers e) (f := ofId S (Localization.AtPrime p.asIdeal)) ⋯
⊢ Eq (α := Set (PrimeSpectrum S))
    (Set.range (ι := PrimeSpectrum (Localization.Away e)) (PrimeSpectrum.comap (algebraMap S (Localization.Away e))))
    {p}

Tactic:
have h₁ := (PrimeSpectrum.localization_away_comap_range (Localization.Away e) e).trans H.symm
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers e) (f := ofId S (Localization.AtPrime p.asIdeal)) ⋯
h₁ :
  Eq (α := Set (PrimeSpectrum S))
    (Set.range (ι := PrimeSpectrum (Localization.Away e)) (PrimeSpectrum.comap (algebraMap S (Localization.Away e))))
    {p}
⊢ Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.Away e))

Tactic:
have : Subsingleton (PrimeSpectrum (Localization.Away e)) :=
    Function.Injective.subsingleton
    (f := Set.codRestrict (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) {p} fun x ↦
      h₁.le ⟨x, rfl⟩)
    ((Set.injective_codRestrict ..).mpr (PrimeSpectrum.localization_comap_injective _ (.powers e)))
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this_2 : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers e) (f := ofId S (Localization.AtPrime p.asIdeal)) ⋯
h₁ :
  Eq (α := Set (PrimeSpectrum S))
    (Set.range (ι := PrimeSpectrum (Localization.Away e)) (PrimeSpectrum.comap (algebraMap S (Localization.Away e))))
    {p}
this : Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.Away e))
x : Localization.AtPrime p.asIdeal
obtain :
  ∀ (x : S) (s : ↥p.asIdeal.primeCompl),
    ∃ (a : Localization.Away e),
      Eq (α := Localization.AtPrime p.asIdeal)
        ((f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal) a : Localization.AtPrime p.asIdeal)
        (IsLocalization.mk' (Localization.AtPrime p.asIdeal) x s : Localization.AtPrime p.asIdeal)
⊢ ∃ (a : Localization.Away e), (f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal) a = x

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

Premises used: Ideal.primeCompl, PrimeSpectrum.asIdeal, rfl, IsLocalization.exists_mk'_eq
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this_2 : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers e) (f := ofId S (Localization.AtPrime p.asIdeal)) ⋯
h₁ :
  Eq (α := Set (PrimeSpectrum S))
    (Set.range (ι := PrimeSpectrum (Localization.Away e)) (PrimeSpectrum.comap (algebraMap S (Localization.Away e))))
    {p}
this_3 : Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
this :
  IsUnit (M := Localization.Away e)
    ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
⊢ ∃ (a : Localization.Away e),
    Eq (α := Localization.AtPrime p.asIdeal)
      ((f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal) a : Localization.AtPrime p.asIdeal)
      (IsLocalization.mk' (Localization.AtPrime p.asIdeal) x s : Localization.AtPrime p.asIdeal)

Tactic:
⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩

Premises used: Units.val, HMul.hMul, Algebra.algebraMap, Inv.inv, Exists.intro, IsUnit.unit, IsUnit.map, IsUnit.mul_right_cancel, DFunLike.coe
-- 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
inst_3 : IsArtinianRing R
p : PrimeSpectrum S
inst_4 : FiniteType R S
H_1 : IsClopen (X := PrimeSpectrum S) {p}
this_1 : IsNoetherianRing S
this_2 : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers e) (f := ofId S (Localization.AtPrime p.asIdeal)) ⋯
h₁ :
  Eq (α := Set (PrimeSpectrum S))
    (Set.range (ι := PrimeSpectrum (Localization.Away e)) (PrimeSpectrum.comap (algebraMap S (Localization.Away e))))
    {p}
this_3 : Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
this :
  IsUnit (M := Localization.Away e)
    ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
refine :
  HMul.hMul (α := Localization.AtPrime p.asIdeal) (β := Localization.AtPrime p.asIdeal)
      ((f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
          (HMul.hMul (α := Localization.Away e)
            ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) x : Localization.Away e)
            (↑this.unit⁻¹ : Localization.Away e)) :
        Localization.AtPrime p.asIdeal)
      ((f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
          ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S)) :
        Localization.AtPrime p.asIdeal) =
    HMul.hMul (α := Localization.AtPrime p.asIdeal) (β := Localization.AtPrime p.asIdeal)
      (IsLocalization.mk' (Localization.AtPrime p.asIdeal) x s : Localization.AtPrime p.asIdeal)
      ((f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
          ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S)) :
        Localization.AtPrime p.asIdeal)
⊢ ∃ (a : Localization.Away e),
    Eq (α := Localization.AtPrime p.asIdeal)
      ((f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal) a : Localization.AtPrime p.asIdeal)
      (IsLocalization.mk' (Localization.AtPrime p.asIdeal) x s : Localization.AtPrime p.asIdeal)

Tactic:
refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩