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
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)
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)
⊢ 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:
simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]

Premises used: mul_assoc, map_mul, IsUnit.val_inv_mul
-- 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)
⊢ (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
-- 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 : S
s : ↥p.asIdeal.primeCompl
suffices :
  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:
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
-- 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 : S
s : ↥p.asIdeal.primeCompl
by_contra :
  ∀
    (H :
      ¬IsUnit (M := Localization.Away e)
          ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)),
    False
⊢ IsUnit (M := Localization.Away e)
    ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)

Tactic:
by_contra 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
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)
⊢ Ne (α := Ideal (Localization.Away e))
    (Ideal.span
      (singleton (α := Localization.Away e)
        ((algebraMap S (Localization.Away e) : (a : S) → Localization.Away e) (↑s : S) : Localization.Away e)))
    ⊤

Tactic:
simpa
-- 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_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)
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
⊢ False

Tactic:
obtain ⟨M, hM, H⟩ :=
      Ideal.exists_le_maximal (.span {algebraMap _ (Localization.Away e) s.1}) (by simpa)

Premises used: Algebra.algebraMap, Localization.Away, Ideal.exists_le_maximal, Ideal.span, Singleton.singleton, Subtype.val, 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_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
⊢ PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
    { asIdeal := M, isPrime := ⋯ }

Tactic:
have := Subsingleton.elim ((IsLocalRing.closedPoint _).comap f.toRingHom) ⟨M, inferInstance⟩
-- 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_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 := ⋯ }
⊢ 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 _))
-- 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_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_4 :
  PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
    { asIdeal := M, isPrime := ⋯ }
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)
⊢ False

Tactic:
simp [IsLocalRing.closedPoint, IsLocalization.AtPrime.isUnit_to_map_iff _ p.asIdeal] at this

Premises used: IsLocalRing.closedPoint, IsLocalization.AtPrime.isUnit_to_map_iff, 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
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))
⊢ 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
-- 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))
hf :
  Function.Surjective (α := Localization.Away e) (β := Localization.AtPrime p.asIdeal)
    (⇑f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
⊢ 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
-- 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))
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)
⊢ Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.AtPrime p.asIdeal))

Tactic:
have := (PrimeSpectrum.comap_injective_of_surjective f.toRingHom hf).subsingleton
-- 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))
hf :
  Function.Surjective (α := Localization.Away e) (β := Localization.AtPrime p.asIdeal)
    (⇑f : (a : Localization.Away e) → Localization.AtPrime p.asIdeal)
this_4 : FiniteType.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
this : Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.AtPrime p.asIdeal))
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
QuasiFinite.iff_finite_comap_preimage_singleton.mpr fun _ ↦
    Set.subsingleton_of_subsingleton.finite

Premises used: Iff.mpr, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, Set.subsingleton_of_subsingleton, Set.Subsingleton.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
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_4 : FiniteType.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
this : Subsingleton.{u_2 + 1} (PrimeSpectrum (Localization.AtPrime p.asIdeal))
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
exact QuasiFinite.iff_finite_comap_preimage_singleton.mpr fun _ ↦
    Set.subsingleton_of_subsingleton.finite

Premises used: Iff.mpr, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, Set.subsingleton_of_subsingleton, Set.Subsingleton.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 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 } ⋯)
⊢ 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