awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ⋯
h₁ :
  Eq (α := Set (PrimeSpectrum S))
    (Set.range (ι := PrimeSpectrum (Localization.Away e)) (PrimeSpectrum.comap (algebraMap S (Localization.Away e))))
    {p}
⊢ QuasiFiniteAt R p.asIdeal
have this₁ : 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)))
-- 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_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
⊢ ∃ (a : Localization.Away e), (f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal) a = x
have 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)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl x
Cleared hypotheses: x
-- 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_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)
have 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)
Tactic: refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩
-- 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_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)
⊢ 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)
have simp : (f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
    (HMul.hMul (α := Localization.Away e) (β := Localization.Away e)
      ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) x : Localization.Away e)
      (1 : Localization.Away e)) =
  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)
Tactic: simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]
-- 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_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 : 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)
have suffices : IsUnit (M := Localization.Away e)
  ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
Tactic: suffices IsUnit (algebraMap _ (Localization.Away e) s.1) by
      refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩
      simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]
      simp
-- 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_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 : S
s : ↥p.asIdeal.primeCompl
⊢ IsUnit (M := Localization.Away e)
    ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
have by_contra : ∀
  (H :
    ¬IsUnit (M := Localization.Away e)
        ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)),
  False
Tactic: by_contra 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
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_2 : {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 : S
s : ↥p.asIdeal.primeCompl
H :
  ¬IsUnit (M := Localization.Away e)
      ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
⊢ False
have obtain : ∀ (M : Ideal (Localization.Away e)) (hM : M.IsMaximal)
  (H :
    Ideal.span
        (singleton (α := Localization.Away e)
          ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)) ≤
      M),
  False
Tactic: obtain ⟨M, hM, H⟩ :=
      Ideal.exists_le_maximal (.span {algebraMap _ (Localization.Away e) s.1}) (by simpa)
-- 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_2 : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H_2 : {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 : S
s : ↥p.asIdeal.primeCompl
H_3 :
  ¬IsUnit (M := Localization.Away e)
      ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
M : Ideal (Localization.Away e)
hM : M.IsMaximal
H :
  Ideal.span
      (singleton (α := Localization.Away e)
        ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)) ≤
    M
⊢ False
have this₁ : PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
  { asIdeal := M, isPrime := sorry }
Tactic: have := Subsingleton.elim ((IsLocalRing.closedPoint _).comap f.toRingHom) ⟨M, inferInstance⟩
-- 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_2 : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H_2 : {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
H_3 :
  ¬IsUnit (M := Localization.Away e)
      ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
M : Ideal (Localization.Away e)
hM : M.IsMaximal
H :
  Ideal.span
      (singleton (α := Localization.Away e)
        ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)) ≤
    M
this :
  PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
    { asIdeal := M, isPrime := ⋯ }
⊢ False
have this₁ : Membership.mem (α := Localization.Away e)
  (PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal))).asIdeal
  ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)
Tactic: have := congr(($this).1).ge (H (Ideal.mem_span_singleton_self _))
-- 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_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))
⊢ QuasiFiniteAt R p.asIdeal
have hf : Function.Surjective (α := Localization.Away e) (β := Localization.AtPrime p.asIdeal)
  (⇑f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
Tactic: have hf : Function.Surjective f := by
    intro x
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl x
    suffices IsUnit (algebraMap _ (Localization.Away e) s.1) by
      refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩
      simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]
      simp
    by_contra H
    obtain ⟨M, hM, H⟩ :=
      Ideal.exists_le_maximal (.span {algebraMap _ (Localization.Away e) s.1}) (by simpa)
    have := Subsingleton.elim ((IsLocalRing.closedPoint _).comap f.toRingHom) ⟨M, inferInstance⟩
    have := congr(($this).1).ge (H (Ideal.mem_span_singleton_self _))
    simp [IsLocalRing.closedPoint, IsLocalization.AtPrime.isUnit_to_map_iff _ p.asIdeal] at this
-- 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_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))
hf :
  Function.Surjective (α := Localization.Away e) (β := Localization.AtPrime p.asIdeal)
    (⇑f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
⊢ QuasiFiniteAt R p.asIdeal
have this₁ : FiniteType.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
Tactic: have : Algebra.FiniteType R (Localization.AtPrime p.asIdeal) :=
    .of_surjective (f.restrictScalars R) hf
-- 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_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))
hf :
  Function.Surjective (α := Localization.Away e) (β := Localization.AtPrime p.asIdeal)
    (⇑f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
this : FiniteType.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
⊢ QuasiFiniteAt R p.asIdeal
have this₁ : Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.AtPrime p.asIdeal))
Tactic: have := (PrimeSpectrum.comap_injective_of_surjective f.toRingHom hf).subsingleton
-- 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 R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
have this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
Tactic: have : Algebra.QuasiFiniteAt p.ResidueField qF.asIdeal := .baseChange q _
    congr($(e.symm_apply_apply ⟨⟨q, ‹_›⟩, PrimeSpectrum.ext (q.over_def p).symm⟩).1.1).symm
-- 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 R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
have obtain : ∀ (r : p.Fiber S) (hr : r ∉ qF.asIdeal)
  (hrq :
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
      {{ asIdeal := qF.asIdeal, isPrime := sorry : PrimeSpectrum (p.Fiber S) }}),
  ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
Tactic: obtain ⟨r, hr, hrq⟩ := Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton
    (R := p.ResidueField) qF.asIdeal
-- 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 R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
have obtain : ∀ (s : R) (hs : s ∉ p) (x : S) (hsx : s • r = 1 ⊗ₜ[R] x),
  ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
Tactic: obtain ⟨s, hs, x, hsx⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ r