awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have 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 }}
Tactic: obtain ⟨r, hrp, H⟩ := IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation
    p.primeCompl (Algebra.linearMap S (Localization.AtPrime p))
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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))
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this₁ : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
Tactic: have : IsLocalization (.powers r) (Localization.AtPrime p) :=
    (isLocalizedModule_iff_isLocalization' _ _).mp H
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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 }}
have 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
Tactic: refine ⟨r, hrp, subset_antisymm (fun q hrq ↦ ?_) (Set.singleton_subset_iff.mpr hrp)⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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))
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }} q
have 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)
Tactic: obtain ⟨q, rfl⟩ := (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r).ge hrq
Cleared hypotheses: q, hrq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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))
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
    (PrimeSpectrum.comap (algebraMap S (Localization.Away r)) q)
have 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))
Tactic: obtain ⟨q, rfl⟩ := (PrimeSpectrum.comapEquiv φ.toRingEquiv).symm.surjective q
Cleared hypotheses: q, hrq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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))
⊢ 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))
have 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))))
Tactic: obtain rfl : q = IsLocalRing.closedPoint _ := Subsingleton.elim _ _
Cleared hypotheses: q, hrq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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))
⊢ 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))))
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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))
⊢ 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
have 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
Tactic: dsimp [-RingEquiv.symm_mk]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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.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
have asIdeal : Ideal.comap (F := S →+* Localization.AtPrime p) (algebraMap S (Localization.AtPrime p))
    (PrimeSpectrum.asIdeal (IsLocalRing.closedPoint (Localization.AtPrime p))) =
  p
Tactic: rw [Ideal.comap_comap, ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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
⊢ IsClopen (X := PrimeSpectrum S) {p}
have this : IsJacobsonRing S
Tactic: have : IsJacobsonRing S := isJacobsonRing_of_finiteType (A := R)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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
⊢ IsClopen (X := PrimeSpectrum S) {p}
have this₁ : IsNoetherianRing S
Tactic: have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing R S
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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}
have refine : IsOpen (X := PrimeSpectrum S) {p}
Tactic: refine ((PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out 0 1).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
⊢ IsOpen (X := PrimeSpectrum S) {p}
have obtain : ∀ (f : S) (hf : f ∉ p.asIdeal)
  (e :
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) =
      {{ asIdeal := p.asIdeal, isPrime := sorry : PrimeSpectrum S }}),
  IsOpen (X := PrimeSpectrum S) {p}
Tactic: obtain ⟨f, hf, e⟩ := exists_basicOpen_eq_singleton (R := R) p.asIdeal
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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}
⊢ QuasiFiniteAt R p.asIdeal
have this : IsNoetherianRing S
Tactic: have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing R S
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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
⊢ QuasiFiniteAt R p.asIdeal
have this₁ : IsJacobsonRing S
Tactic: have : IsJacobsonRing S := isJacobsonRing_of_finiteType (A := R)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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
⊢ QuasiFiniteAt R p.asIdeal
have H₁ : IsClopen (X := PrimeSpectrum S) {p}
Tactic: rw [(PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out
    0 1 rfl rfl] at H
Cleared hypotheses: H, this_1, this
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
⊢ QuasiFiniteAt R p.asIdeal
have obtain : ∀ (e : S) (he : IsIdempotentElem e) (H : {p} = (↑(PrimeSpectrum.basicOpen e) : Set (PrimeSpectrum S))),
  QuasiFiniteAt R p.asIdeal
Tactic: obtain ⟨e, he, H⟩ := PrimeSpectrum.isClopen_iff.mp H
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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))
⊢ QuasiFiniteAt R p.asIdeal
have hep : e ∉ p.asIdeal
Tactic: have hep : e ∉ p.asIdeal := H.le rfl
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
⊢ ∀ (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)
have 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)
Tactic: simp only [Subtype.forall]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
have 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
Tactic: refine Submonoid.powers_le (P := (IsUnit.submonoid _).comap _).mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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)) ⋯
⊢ QuasiFiniteAt R p.asIdeal
have h₁ : 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