-- Mathlib/RingTheory/Trace/Quotient.lean
lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
    (Ideal.map (algebraMap R Sₚ) p).comap (algebraMap S Sₚ) = pS

Proof state:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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 + γ

Tactic:
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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 + γ

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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γ : γ ∈ p
hβ : β * α = 1 + γ
this : x + γ • x ∈ pS
⊢ (algebraMap R S) γ * x ∈ pS

Tactic:
apply Ideal.mul_mem_right

Result:
case intro.intro.intro.intro.intro.h
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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γ : γ ∈ p
hβ : β * α = 1 + γ
this : x + γ • x ∈ pS
⊢ (algebraMap R S) γ ∈ pS

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * ↑(y, s).1 ∈ pS

Tactic:
exact Ideal.mul_mem_left _ _ y.prop

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ α • x ∈ pS

Tactic:
rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * ↑(y, s).1 ∈ pS

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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γ : γ ∈ p
hβ : β * α = 1 + γ
this : (algebraMap R S) β * α • x ∈ pS
⊢ x ∈ pS

Tactic:
rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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γ : γ ∈ p
hβ : β * α = 1 + γ
this : x + γ • x ∈ pS
⊢ x ∈ pS

Proof state:
case intro.refine_1
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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) α)⁻¹
⊢ β * α - 1 ∈ p

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
  map_mul, hβ, inv_mul_cancel₀, sub_self]

Result:
case intro.refine_1
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S 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) α)⁻¹
⊢ (Ideal.Quotient.mk p) α ≠ 0