case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y ∈ I
⊢ ↑(algebraMap R S) x ∈ I

case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : ↑(algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
⊢ mk' S x y ∈ I ↔ ↑(algebraMap R S) x ∈ I
constructor <;> intro h
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y ∈ I
⊢ ↑(algebraMap R S) ↑y * mk' S x y ∈ I
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y ∈ I
⊢ ↑(algebraMap R S) x ∈ I
rw [← mk'_spec S x y, mul_comm]
no goals
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y ∈ I
⊢ ↑(algebraMap R S) ↑y * mk' S x y ∈ I
exact I.mul_mem_left ((algebraMap R S) y) h
case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y * ↑(algebraMap R S) ↑y ∈ I
⊢ mk' S x y ∈ I
case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : ↑(algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I
rw [← mk'_spec S x y] at h
case mpr.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y * ↑(algebraMap R S) ↑y ∈ I
b : S
hb : ↑(algebraMap R S) ↑y * b = 1
⊢ mk' S x y ∈ I
case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y * ↑(algebraMap R S) ↑y ∈ I
⊢ mk' S x y ∈ I
obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)
case mpr.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y * ↑(algebraMap R S) ↑y ∈ I
b : S
hb : ↑(algebraMap R S) ↑y * b = 1
this : b * (mk' S x y * ↑(algebraMap R S) ↑y) ∈ I
⊢ mk' S x y ∈ I
case mpr.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y * ↑(algebraMap R S) ↑y ∈ I
b : S
hb : ↑(algebraMap R S) ↑y * b = 1
⊢ mk' S x y ∈ I
have := I.mul_mem_left b h
no goals
case mpr.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.672634
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
I : Ideal S
h : mk' S x y * ↑(algebraMap R S) ↑y ∈ I
b : S
hb : ↑(algebraMap R S) ↑y * b = 1
this : b * (mk' S x y * ↑(algebraMap R S) ↑y) ∈ I
⊢ mk' S x y ∈ I
rwa [mul_comm, mul_assoc, hb, mul_one] at this