case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst

case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) → z ∈ Ideal.map (algebraMap R S) I
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst
constructor
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → z ∈ IsLocalization.map_ideal M S I
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst
change _ → z ∈ map_ideal M S I
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
hz : z ∈ ↑(algebraMap R S) '' ↑I
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → z ∈ IsLocalization.map_ideal M S I
refine' fun h => Ideal.mem_sInf.1 h fun z hz => _
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ ↑(algebraMap R S) y = z
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
hz : z ∈ ↑(algebraMap R S) '' ↑I
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)
obtain ⟨y, hy⟩ := hz
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ ↑(algebraMap R S) y = z
Z : { x // x ∈ I } := { val := y, property := (_ : y ∈ ↑I) }
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ ↑(algebraMap R S) y = z
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)
let Z : { x // x ∈ I } := ⟨y, hy.left⟩
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ ↑(algebraMap R S) y = z
Z : { x // x ∈ I } := { val := y, property := (_ : y ∈ ↑I) }
⊢ z * ↑(algebraMap R S) ↑(Z, 1).snd = ↑(algebraMap R S) ↑(Z, 1).fst
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ ↑(algebraMap R S) y = z
Z : { x // x ∈ I } := { val := y, property := (_ : y ∈ ↑I) }
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)
use ⟨Z, 1⟩
no goals
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ ↑(algebraMap R S) y = z
Z : { x // x ∈ I } := { val := y, property := (_ : y ∈ ↑I) }
⊢ z * ↑(algebraMap R S) ↑(Z, 1).snd = ↑(algebraMap R S) ↑(Z, 1).fst
simp [hy.right]
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : { x // x ∈ I }
s : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑(a, s).snd = ↑(algebraMap R S) ↑(a, s).fst
⊢ z ∈ Ideal.map (algebraMap R S) I
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) → z ∈ Ideal.map (algebraMap R S) I
rintro ⟨⟨a, s⟩, h⟩
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : { x // x ∈ I }
s : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑(a, s).snd = ↑(algebraMap R S) ↑(a, s).fst
⊢ z * ↑(algebraMap R S) ↑s ∈ Ideal.map (algebraMap R S) I
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : { x // x ∈ I }
s : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑(a, s).snd = ↑(algebraMap R S) ↑(a, s).fst
⊢ z ∈ Ideal.map (algebraMap R S) I
rw [← Ideal.unit_mul_mem_iff_mem _ (map_units S s), mul_comm]
no goals
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : { x // x ∈ I }
s : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑(a, s).snd = ↑(algebraMap R S) ↑(a, s).fst
⊢ z * ↑(algebraMap R S) ↑s ∈ Ideal.map (algebraMap R S) I
exact h.symm ▸ Ideal.mem_map_of_mem _ a.2