awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
h :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
h₁ :
  HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
      ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
⊢ HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
      ((algebraMap S Sₚ : (a : S) → Sₚ)
          (↑(Subtype.mk (p := fun (x : S) ↦
                    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x) (γ • x) ⋯,
                  s).2 :
            S) :
        Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ)
      (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x)
                (γ • x) ⋯,
              s).1 :
        S)

Tactic:
simp only
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalization.AtPrime S p
hle : ¬I ≤ p
hle₁ : ¬(↑I : Set R) ⊆ (↑p.primeCompl : Set R)ᶜ
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤

Tactic:
apply IsLocalization.map_eq_top_of_not_subset p.primeCompl

Premises used: IsLocalization.map_eq_top_of_not_subset, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalization.AtPrime S p
hle : ¬I ≤ p
⊢ ¬(↑I : Set R) ⊆ (↑p.primeCompl : Set R)ᶜ

Tactic:
simpa [SetLike.le_def, Set.not_subset_iff_exists_mem_notMem] using hle

Premises used: Set.not_subset_iff_exists_mem_notMem, SetLike.le_def
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
⊢ Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) Q

Tactic:
⟨inferInstance, ?_⟩

Premises used: Ideal.primesOver, Set.Mem, setOf, inferInstance, And.intro
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
refine : Q.LiesOver (maximalIdeal Rₚ)
⊢ Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) Q

Tactic:
refine ⟨inferInstance, ?_⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
rw : IsMaximal (under Rₚ Q)
⊢ Q.LiesOver (maximalIdeal Rₚ)

Tactic:
rw [liesOver_iff, ← eq_maximalIdeal]

Premises used: Ideal.liesOver_iff, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
⊢ IsMaximal (under Rₚ Q)

Tactic:
IsMaximal.under Rₚ Q

Premises used: Ideal.IsMaximal.under
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
⊢ IsMaximal (under Rₚ Q)

Tactic:
exact IsMaximal.under Rₚ Q

Premises used: Ideal.IsMaximal.under
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
⊢ LiesOver (maximalIdeal Rₚ) p

Tactic:
have : (maximalIdeal Rₚ).LiesOver p := liesOver_maximalIdeal Rₚ p _
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
this : LiesOver (maximalIdeal Rₚ) p
⊢ Q.LiesOver p

Tactic:
LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p

Premises used: IsLocalRing.maximalIdeal, Ideal.LiesOver.trans
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
this : LiesOver (maximalIdeal Rₚ) p
⊢ Q.LiesOver p

Tactic:
exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p

Premises used: IsLocalRing.maximalIdeal, Ideal.LiesOver.trans
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := by
    have : (maximalIdeal Rₚ).LiesOver p := liesOver_maximalIdeal Rₚ p _
    exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
this : Q.LiesOver p
⊢ LiesOver (comap (F := S →+* T) (algebraMap S T) Q) p

Tactic:
comap_liesOver Q p <| IsScalarTower.toAlgHom R S T

Premises used: IsScalarTower.toAlgHom, Ideal.comap_liesOver, Ideal.comap
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
this : Q.LiesOver p
⊢ LiesOver (comap (F := S →+* T) (algebraMap S T) Q) p

Tactic:
exact comap_liesOver Q p <| IsScalarTower.toAlgHom R S T

Premises used: IsScalarTower.toAlgHom, Ideal.comap_liesOver
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : P.IsPrime
rw :
  Eq (α := Ideal Rₚ) (under.{u_3, u_4} Rₚ (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R P))
⊢ LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)

Tactic:
rw [liesOver_iff, eq_comm, ← map_eq_maximalIdeal p, over_def P p]

Premises used: Ideal.liesOver_iff, eq_comm, IsLocalization.AtPrime.map_eq_maximalIdeal, Ideal.over_def
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : P.IsPrime
⊢ Eq (α := Ideal Rₚ) (under.{u_3, u_4} Rₚ (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R P))

Tactic:
under_map_eq_map_under _
    (over_def P p ▸ map_eq_maximalIdeal p Rₚ ▸ maximalIdeal.isMaximal Rₚ)
    (isPrime_map_of_liesOver S p Sₚ P).ne_top

Premises used: Eq.rec, IsLocalization.AtPrime.map_eq_maximalIdeal, IsLocalRing.maximalIdeal.isMaximal, Ideal.over_def, Ideal.under_map_eq_map_under, Eq.symm, Ideal.IsPrime.ne_top, IsLocalization.AtPrime.isPrime_map_of_liesOver
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : P.IsPrime
⊢ Eq (α := Ideal Rₚ) (under.{u_3, u_4} Rₚ (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R P))

Tactic:
exact under_map_eq_map_under _
    (over_def P p ▸ map_eq_maximalIdeal p Rₚ ▸ maximalIdeal.isMaximal Rₚ)
    (isPrime_map_of_liesOver S p Sₚ P).ne_top

Premises used: Ideal.under_map_eq_map_under, Ideal.IsPrime.ne_top, IsLocalization.AtPrime.isPrime_map_of_liesOver
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
obtain :
  ∀ (x : Sₚ),
    ∃ (a : S),
      Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
              (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            a :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
              (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            x :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ∃ (a : S),
    (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
          (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        a =
      x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : Sₚ
obtain :
  ∀ (x : S) (s : ↥(algebraMapSubmonoid S p.primeCompl)),
    ∃ (a : S),
      Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
              (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            a :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
              (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            (mk' Sₚ x s) :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          x :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (algebraMapSubmonoid S p.primeCompl) x

Premises used: Ideal.primeCompl, Algebra.algebraMapSubmonoid, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
obtain :
  ∀ (s' : S)
    (hs :
      Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
        (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)),
    ∃ (a : S),
      Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
              (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            a :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
              (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            (mk' Sₚ x s) :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))

Tactic:
obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := P) (Ideal.Quotient.mk P s)⁻¹

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Inv.inv, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
simp :
  ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((algebraMap S Sₚ : (a : S) → Sₚ) a) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))

Tactic:
simp only [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), Quotient.algebraMap_eq, RingHom.comp_apply]

Premises used: Ideal.Quotient.algebraMap_eq, HasQuotient.Quotient, IsScalarTower.algebraMap_eq, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h :
  Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s')) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((algebraMap S Sₚ : (a : S) → Sₚ) a) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))

Tactic:
use x * s'
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))
⊢ Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s')) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))

Tactic:
rw [← sub_eq_zero, ← map_sub, Quotient.eq_zero_iff_mem]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
⊢ IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)

Tactic:
have h₀ : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P