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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
⊢ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) ≤ 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
⊢ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I
refine' le_antisymm _ Ideal.le_comap_map
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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
⊢ a ∈ 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
⊢ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) ≤ I
refine' (fun a ha => _)
case 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) a * ↑(algebraMap R S) ↑(b, s).snd = ↑(algebraMap R S) ↑(b, s).fst
⊢ a ∈ 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
⊢ a ∈ I
obtain ⟨⟨b, s⟩, h⟩ := (mem_map_algebraMap_iff M S).1 (Ideal.mem_comap.1 ha)
case 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
⊢ a ∈ I
case 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) a * ↑(algebraMap R S) ↑(b, s).snd = ↑(algebraMap R S) ↑(b, s).fst
⊢ a ∈ I
replace h : algebraMap R S (s * a) = algebraMap R S b := by
  simpa only [← map_mul, mul_comm] using h
case intro.mk.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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ a ∈ I
case 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
⊢ a ∈ I
obtain ⟨c, hc⟩ := (eq_iff_exists M S).1 h
case intro.mk.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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
this : ↑c * ↑s * a ∈ I
⊢ a ∈ I
case intro.mk.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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ a ∈ I
have : ↑c * ↑s * a ∈ I := by
  rw [mul_assoc, hc]
  exact I.mul_mem_left c b.2
no goals
case intro.mk.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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
this : ↑c * ↑s * a ∈ I
⊢ a ∈ I
exact (hI.mem_or_mem this).resolve_left fun hsc => hM.le_bot ⟨(c * s).2, hsc⟩
no goals
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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) a * ↑(algebraMap R S) ↑(b, s).snd = ↑(algebraMap R S) ↑(b, s).fst
⊢ ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
simpa only [← map_mul, mul_comm] using h
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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ ↑c * ↑b ∈ 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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ ↑c * ↑s * a ∈ I
rw [mul_assoc, hc]
no goals
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
hI : Ideal.IsPrime I
hM : Disjoint ↑M ↑I
a : R
ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)
b : { x // x ∈ I }
s : { x // x ∈ M }
h : ↑(algebraMap R S) (↑s * a) = ↑(algebraMap R S) ↑b
c : { x // x ∈ M }
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ ↑c * ↑b ∈ I
exact I.mul_mem_left c b.2