obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
R : Type u_3
S : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsMaximal
Rₚ : Type ?u.245679
Sₚ : Type u_2
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization.AtPrime Rₚ p
inst✝⁷ : LocalRing Rₚ
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
⊢ ∃ β, ∃ γ ∈ p, β * α = 1 + γ
case intro
R : Type u_3
S : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsMaximal
Rₚ : Type ?u.245679
Sₚ : Type u_2
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization.AtPrime Rₚ p
inst✝⁷ : LocalRing Rₚ
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ ∃ β, ∃ γ ∈ p, β * α = 1 + γ