-- 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ₚ
⊢ pS = Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)

Tactic:
apply Ideal.le_comap_map.antisymm

Result:
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ₚ
⊢ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS) ≤ 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)
y : ↥pS
s : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)
hy : (algebraMap S Sₚ) x * (algebraMap S Sₚ) ↑(y, s).2 = (algebraMap S Sₚ) ↑(y, s).1
⊢ ∃ α ∉ p, α • x ∈ pS

Tactic:
rw [← map_mul,
  IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy

Result:
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 : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)
hy : ∃ c, ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
⊢ ∃ α ∉ p, α • x ∈ 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)
⊢ ∃ α ∉ p, α • x ∈ pS

Tactic:
refine ⟨α, hα, ?_⟩

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)
⊢ α • 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) α)⁻¹
⊢ (Ideal.Quotient.mk p) α ≠ 0

Tactic:
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]

Result:
no goals

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ₚ
⊢ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS) ≤ pS

Tactic:
intro x hx

Result:
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)
⊢ x ∈ pS

Proof state:
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)
y : ↥pS
s c : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
⊢ ∃ α ∉ p, α • x ∈ pS

Tactic:
obtain ⟨α, hα, e⟩ := (c * s).prop

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)
⊢ ∃ α ∉ p, α • x ∈ 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ₚ
⊢ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap R Sₚ) p) = pS

Tactic:
rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]

Result:
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ₚ
⊢ pS = Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)

Proof state:
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

Tactic:
exact Ideal.mem_map_of_mem _ hγ

Result:
no goals