[GOAL]
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
⊢ ∀ {a b : S},
    a ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
      b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
        a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}
[PROOFSTEP]
rintro a b ⟨a', ha⟩ ⟨b', hb⟩
[GOAL]
case intro.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
a b : S
a' : { x // x ∈ I } × { x // x ∈ M }
ha : a * ↑(algebraMap R S) ↑a'.snd = ↑(algebraMap R S) ↑a'.fst
b' : { x // x ∈ I } × { x // x ∈ M }
hb : b * ↑(algebraMap R S) ↑b'.snd = ↑(algebraMap R S) ↑b'.fst
⊢ a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}
[PROOFSTEP]
let Z : { x // x ∈ I } :=
  ⟨(a'.2 : R) * (b'.1 : R) + (b'.2 : R) * (a'.1 : R), I.add_mem (I.mul_mem_left _ b'.1.2) (I.mul_mem_left _ a'.1.2)⟩
[GOAL]
case intro.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
a b : S
a' : { x // x ∈ I } × { x // x ∈ M }
ha : a * ↑(algebraMap R S) ↑a'.snd = ↑(algebraMap R S) ↑a'.fst
b' : { x // x ∈ I } × { x // x ∈ M }
hb : b * ↑(algebraMap R S) ↑b'.snd = ↑(algebraMap R S) ↑b'.fst
Z : { x // x ∈ I } :=
  { val := ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst, property := (_ : ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst ∈ I) }
⊢ a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}
[PROOFSTEP]
use⟨Z, a'.2 * b'.2⟩
[GOAL]
case 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
a b : S
a' : { x // x ∈ I } × { x // x ∈ M }
ha : a * ↑(algebraMap R S) ↑a'.snd = ↑(algebraMap R S) ↑a'.fst
b' : { x // x ∈ I } × { x // x ∈ M }
hb : b * ↑(algebraMap R S) ↑b'.snd = ↑(algebraMap R S) ↑b'.fst
Z : { x // x ∈ I } :=
  { val := ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst, property := (_ : ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst ∈ I) }
⊢ (a + b) * ↑(algebraMap R S) ↑(Z, a'.snd * b'.snd).snd = ↑(algebraMap R S) ↑(Z, a'.snd * b'.snd).fst
[PROOFSTEP]
simp only [RingHom.map_add, Submodule.coe_mk, Submonoid.coe_mul, RingHom.map_mul]
[GOAL]
case 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
a b : S
a' : { x // x ∈ I } × { x // x ∈ M }
ha : a * ↑(algebraMap R S) ↑a'.snd = ↑(algebraMap R S) ↑a'.fst
b' : { x // x ∈ I } × { x // x ∈ M }
hb : b * ↑(algebraMap R S) ↑b'.snd = ↑(algebraMap R S) ↑b'.fst
Z : { x // x ∈ I } :=
  { val := ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst, property := (_ : ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst ∈ I) }
⊢ (a + b) * (↑(algebraMap R S) ↑a'.snd * ↑(algebraMap R S) ↑b'.snd) =
    ↑(algebraMap R S) ↑a'.snd * ↑(algebraMap R S) ↑b'.fst + ↑(algebraMap R S) ↑b'.snd * ↑(algebraMap R S) ↑a'.fst
[PROOFSTEP]
rw [add_mul, ← mul_assoc a, ha, mul_comm (algebraMap R S a'.2) (algebraMap R S b'.2), ← mul_assoc b, hb]
[GOAL]
case 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
a b : S
a' : { x // x ∈ I } × { x // x ∈ M }
ha : a * ↑(algebraMap R S) ↑a'.snd = ↑(algebraMap R S) ↑a'.fst
b' : { x // x ∈ I } × { x // x ∈ M }
hb : b * ↑(algebraMap R S) ↑b'.snd = ↑(algebraMap R S) ↑b'.fst
Z : { x // x ∈ I } :=
  { val := ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst, property := (_ : ↑a'.snd * ↑b'.fst + ↑b'.snd * ↑a'.fst ∈ I) }
⊢ ↑(algebraMap R S) ↑a'.fst * ↑(algebraMap R S) ↑b'.snd + ↑(algebraMap R S) ↑b'.fst * ↑(algebraMap R S) ↑a'.snd =
    ↑(algebraMap R S) ↑a'.snd * ↑(algebraMap R S) ↑b'.fst + ↑(algebraMap R S) ↑b'.snd * ↑(algebraMap R S) ↑a'.fst
[PROOFSTEP]
ring
[GOAL]
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
⊢ 0 * ↑(algebraMap R S) ↑(0, 1).snd = ↑(algebraMap R S) ↑(0, 1).fst
[PROOFSTEP]
simp
[GOAL]
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
⊢ ∀ (c : S) {x : S},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst},
                  add_mem' :=
                    (_ :
                      ∀ {a b : S},
                        a ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                          b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                            a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}) },
              zero_mem' :=
                (_ : ∃ x, 0 * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst},
                  add_mem' :=
                    (_ :
                      ∀ {a b : S},
                        a ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                          b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                            a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}) },
              zero_mem' :=
                (_ : ∃ x, 0 * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro c x ⟨x', hx⟩
[GOAL]
case 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
c x : S
x' : { x // x ∈ I } × { x // x ∈ M }
hx : x * ↑(algebraMap R S) ↑x'.snd = ↑(algebraMap R S) ↑x'.fst
⊢ c • x ∈
    {
          toAddSubsemigroup :=
            { carrier := {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst},
              add_mem' :=
                (_ :
                  ∀ {a b : S},
                    a ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                      b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                        a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}) },
          zero_mem' := (_ : ∃ x, 0 * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) }.toAddSubsemigroup.carrier
[PROOFSTEP]
obtain ⟨c', hc⟩ := IsLocalization.surj M c
[GOAL]
case intro.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
c x : S
x' : { x // x ∈ I } × { x // x ∈ M }
hx : x * ↑(algebraMap R S) ↑x'.snd = ↑(algebraMap R S) ↑x'.fst
c' : R × { x // x ∈ M }
hc : c * ↑(algebraMap R S) ↑c'.snd = ↑(algebraMap R S) c'.fst
⊢ c • x ∈
    {
          toAddSubsemigroup :=
            { carrier := {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst},
              add_mem' :=
                (_ :
                  ∀ {a b : S},
                    a ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                      b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                        a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}) },
          zero_mem' := (_ : ∃ x, 0 * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) }.toAddSubsemigroup.carrier
[PROOFSTEP]
let Z : { x // x ∈ I } := ⟨c'.1 * x'.1, I.mul_mem_left c'.1 x'.1.2⟩
[GOAL]
case intro.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
c x : S
x' : { x // x ∈ I } × { x // x ∈ M }
hx : x * ↑(algebraMap R S) ↑x'.snd = ↑(algebraMap R S) ↑x'.fst
c' : R × { x // x ∈ M }
hc : c * ↑(algebraMap R S) ↑c'.snd = ↑(algebraMap R S) c'.fst
Z : { x // x ∈ I } := { val := c'.fst * ↑x'.fst, property := (_ : c'.fst * ↑x'.fst ∈ I) }
⊢ c • x ∈
    {
          toAddSubsemigroup :=
            { carrier := {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst},
              add_mem' :=
                (_ :
                  ∀ {a b : S},
                    a ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                      b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst} →
                        a + b ∈ {z | ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst}) },
          zero_mem' := (_ : ∃ x, 0 * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst) }.toAddSubsemigroup.carrier
[PROOFSTEP]
use⟨Z, c'.2 * x'.2⟩
[GOAL]
case 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
c x : S
x' : { x // x ∈ I } × { x // x ∈ M }
hx : x * ↑(algebraMap R S) ↑x'.snd = ↑(algebraMap R S) ↑x'.fst
c' : R × { x // x ∈ M }
hc : c * ↑(algebraMap R S) ↑c'.snd = ↑(algebraMap R S) c'.fst
Z : { x // x ∈ I } := { val := c'.fst * ↑x'.fst, property := (_ : c'.fst * ↑x'.fst ∈ I) }
⊢ c • x * ↑(algebraMap R S) ↑(Z, c'.snd * x'.snd).snd = ↑(algebraMap R S) ↑(Z, c'.snd * x'.snd).fst
[PROOFSTEP]
simp only [← hx, ← hc, smul_eq_mul, Submodule.coe_mk, Submonoid.coe_mul, RingHom.map_mul]
[GOAL]
case 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
c x : S
x' : { x // x ∈ I } × { x // x ∈ M }
hx : x * ↑(algebraMap R S) ↑x'.snd = ↑(algebraMap R S) ↑x'.fst
c' : R × { x // x ∈ M }
hc : c * ↑(algebraMap R S) ↑c'.snd = ↑(algebraMap R S) c'.fst
Z : { x // x ∈ I } := { val := c'.fst * ↑x'.fst, property := (_ : c'.fst * ↑x'.fst ∈ I) }
⊢ c * x * (↑(algebraMap R S) ↑c'.snd * ↑(algebraMap R S) ↑x'.snd) =
    c * ↑(algebraMap R S) ↑c'.snd * (x * ↑(algebraMap R S) ↑x'.snd)
[PROOFSTEP]
ring
  -- Porting note: removed #align declaration since it is a private def
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
change _ → z ∈ map_ideal M S I
[GOAL]
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
[PROOFSTEP]
refine' fun h => Ideal.mem_sInf.1 h fun z hz => _
[GOAL]
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)
[PROOFSTEP]
obtain ⟨y, hy⟩ := hz
[GOAL]
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)
[PROOFSTEP]
let Z : { x // x ∈ I } := ⟨y, hy.left⟩
[GOAL]
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)
[PROOFSTEP]
use⟨Z, 1⟩
[GOAL]
case 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
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
[PROOFSTEP]
simp [hy.right]
[GOAL]
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
[PROOFSTEP]
rintro ⟨⟨a, s⟩, h⟩
[GOAL]
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
[PROOFSTEP]
rw [← Ideal.unit_mul_mem_iff_mem _ (map_units S s), mul_comm]
[GOAL]
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
[PROOFSTEP]
exact h.symm ▸ Ideal.mem_map_of_mem _ a.2
[GOAL]
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
J : Ideal S
x : S
hJ : x ∈ J
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
[PROOFSTEP]
obtain ⟨r, s, hx⟩ := mk'_surjective M x
[GOAL]
case intro.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
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : { x // x ∈ M }
hx : mk' S r s = x
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
[PROOFSTEP]
rw [← hx] at hJ ⊢
[GOAL]
case intro.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
J : Ideal S
x : S
r : R
s : { x // x ∈ M }
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
[PROOFSTEP]
exact
  Ideal.mul_mem_right _ _
    (Ideal.mem_map_of_mem _ (show (algebraMap R S) r ∈ J from mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))
[GOAL]
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
[PROOFSTEP]
refine' le_antisymm _ Ideal.le_comap_map
[GOAL]
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
[PROOFSTEP]
refine' (fun a ha => _)
[GOAL]
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
[PROOFSTEP]
obtain ⟨⟨b, s⟩, h⟩ := (mem_map_algebraMap_iff M S).1 (Ideal.mem_comap.1 ha)
[GOAL]
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
[PROOFSTEP]
replace h : algebraMap R S (s * a) = algebraMap R S b := by simpa only [← map_mul, mul_comm] using h
[GOAL]
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
[PROOFSTEP]
simpa only [← map_mul, mul_comm] using h
[GOAL]
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
[PROOFSTEP]
obtain ⟨c, hc⟩ := (eq_iff_exists M S).1 h
[GOAL]
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
[PROOFSTEP]
have : ↑c * ↑s * a ∈ I := by
  rw [mul_assoc, hc]
  exact I.mul_mem_left c b.2
[GOAL]
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
[PROOFSTEP]
rw [mul_assoc, hc]
[GOAL]
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
[PROOFSTEP]
exact I.mul_mem_left c b.2
[GOAL]
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
[PROOFSTEP]
exact (hI.mem_or_mem this).resolve_left fun hsc => hM.le_bot ⟨(c * s).2, hsc⟩
[GOAL]
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
⊢ ∀ {a b : Ideal S},
    ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
              inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
          a ≤
        ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
              inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro J₁ J₂
[GOAL]
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
J₁ J₂ : Ideal S
⊢ ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₁ ≤
      ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₂ ↔
    J₁ ≤ J₂
[PROOFSTEP]
constructor
[GOAL]
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
J₁ J₂ : Ideal S
⊢ ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₁ ≤
      ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₂ →
    J₁ ≤ J₂
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
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ →
    ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₁ ≤
      ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₂
[PROOFSTEP]
exact (fun hJ => (map_comap M S) J₁ ▸ (map_comap M S) J₂ ▸ Ideal.map_mono hJ)
[GOAL]
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
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ →
    ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₁ ≤
      ↑{ toFun := fun J => Ideal.comap (algebraMap R S) J,
            inj' := (_ : Function.Injective fun J => Ideal.comap (algebraMap R S) J) }
        J₂
[PROOFSTEP]
exact (fun hJ => Ideal.comap_mono hJ)
[GOAL]
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
J : Ideal S
⊢ Ideal.IsPrime J ↔ Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
[PROOFSTEP]
constructor
[GOAL]
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
J : Ideal S
⊢ Ideal.IsPrime J → Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
[PROOFSTEP]
refine' fun h =>
  ⟨⟨_, _⟩, Set.disjoint_left.mpr fun m hm1 hm2 => h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
[GOAL]
case mp.refine'_1
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
J : Ideal S
h : Ideal.IsPrime J
⊢ Ideal.comap (algebraMap R S) J ≠ ⊤
[PROOFSTEP]
refine' fun hJ => h.ne_top _
[GOAL]
case mp.refine'_1
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
J : Ideal S
h : Ideal.IsPrime J
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ J = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
[GOAL]
case mp.refine'_1
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
J : Ideal S
h : Ideal.IsPrime J
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ ↑(orderEmbedding M S) ⊤ ≤ ↑(orderEmbedding M S) J
[PROOFSTEP]
exact le_of_eq hJ.symm
[GOAL]
case mp.refine'_2
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
J : Ideal S
h : Ideal.IsPrime J
⊢ ∀ {x y : R},
    x * y ∈ Ideal.comap (algebraMap R S) J → x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J
[PROOFSTEP]
intro x y hxy
[GOAL]
case mp.refine'_2
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
J : Ideal S
h : Ideal.IsPrime J
x y : R
hxy : x * y ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J
[PROOFSTEP]
rw [Ideal.mem_comap, RingHom.map_mul] at hxy 
[GOAL]
case mp.refine'_2
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
J : Ideal S
h : Ideal.IsPrime J
x y : R
hxy : ↑(algebraMap R S) x * ↑(algebraMap R S) y ∈ J
⊢ x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J
[PROOFSTEP]
exact h.mem_or_mem hxy
[GOAL]
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
J : Ideal S
⊢ Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J) → Ideal.IsPrime J
[PROOFSTEP]
refine' fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 _), _⟩
[GOAL]
case mpr.refine'_1
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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.comap (algebraMap R S) J
[PROOFSTEP]
rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ 
[GOAL]
case mpr.refine'_2
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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J
[PROOFSTEP]
intro x y hxy
[GOAL]
case mpr.refine'_2
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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
obtain ⟨a, s, ha⟩ := mk'_surjective M x
[GOAL]
case mpr.refine'_2.intro.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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
obtain ⟨b, t, hb⟩ := mk'_surjective M y
[GOAL]
case mpr.refine'_2.intro.intro.intro.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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
[GOAL]
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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
⊢ mk' S (a * b) (s * t) ∈ J
[PROOFSTEP]
rwa [mk'_mul, ha, hb]
[GOAL]
case mpr.refine'_2.intro.intro.intro.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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
rw [mk'_mem_iff, ← Ideal.mem_comap] at this 
[GOAL]
case mpr.refine'_2.intro.intro.intro.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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
[GOAL]
case mpr.refine'_2.intro.intro.intro.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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
this₂ : a ∈ Ideal.comap (algebraMap R S) J ∨ b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
rw [Ideal.mem_comap, Ideal.mem_comap] at this₂ 
[GOAL]
case mpr.refine'_2.intro.intro.intro.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
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
this₂ : ↑(algebraMap R S) a ∈ J ∨ ↑(algebraMap R S) b ∈ J
⊢ x ∈ J ∨ y ∈ J
[PROOFSTEP]
rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]
[GOAL]
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
hp : Ideal.IsPrime I
hd : Disjoint ↑M ↑I
⊢ Ideal.IsPrime (Ideal.map (algebraMap R S) I)
[PROOFSTEP]
rw [isPrime_iff_isPrime_disjoint M S, comap_map_of_isPrime_disjoint M S I hp hd]
[GOAL]
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
hp : Ideal.IsPrime I
hd : Disjoint ↑M ↑I
⊢ Ideal.IsPrime I ∧ Disjoint ↑M ↑I
[PROOFSTEP]
exact ⟨hp, hd⟩
[GOAL]
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
⊢ ∀ {a b : { p // Ideal.IsPrime p }},
    ↑{
              toFun := fun p =>
                { val := Ideal.comap (algebraMap R S) ↑p,
                  property :=
                    (_ :
                      Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                        Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
              invFun := fun p =>
                { val := Ideal.map (algebraMap R S) ↑p,
                  property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
              left_inv :=
                (_ :
                  ∀ (J : { p // Ideal.IsPrime p }),
                    (fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        ((fun p =>
                            { val := Ideal.comap (algebraMap R S) ↑p,
                              property :=
                                (_ :
                                  Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                    Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                          J) =
                      J),
              right_inv :=
                (_ :
                  ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                    (fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        ((fun p =>
                            { val := Ideal.map (algebraMap R S) ↑p,
                              property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                          I) =
                      I) }
          a ≤
        ↑{
              toFun := fun p =>
                { val := Ideal.comap (algebraMap R S) ↑p,
                  property :=
                    (_ :
                      Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                        Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
              invFun := fun p =>
                { val := Ideal.map (algebraMap R S) ↑p,
                  property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
              left_inv :=
                (_ :
                  ∀ (J : { p // Ideal.IsPrime p }),
                    (fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        ((fun p =>
                            { val := Ideal.comap (algebraMap R S) ↑p,
                              property :=
                                (_ :
                                  Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                    Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                          J) =
                      J),
              right_inv :=
                (_ :
                  ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                    (fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        ((fun p =>
                            { val := Ideal.map (algebraMap R S) ↑p,
                              property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                          I) =
                      I) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro I I'
[GOAL]
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 I' : { p // Ideal.IsPrime p }
⊢ ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I ≤
      ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I' ↔
    I ≤ I'
[PROOFSTEP]
constructor
[GOAL]
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 I' : { p // Ideal.IsPrime p }
⊢ ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I ≤
      ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I' →
    I ≤ 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 I' : { p // Ideal.IsPrime p }
⊢ I ≤ I' →
    ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I ≤
      ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I'
[PROOFSTEP]
exact (fun h => show I.val ≤ I'.val from map_comap M S I.val ▸ map_comap M S I'.val ▸ Ideal.map_mono h)
[GOAL]
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 I' : { p // Ideal.IsPrime p }
⊢ I ≤ I' →
    ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I ≤
      ↑{
            toFun := fun p =>
              { val := Ideal.comap (algebraMap R S) ↑p,
                property :=
                  (_ :
                    Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) },
            invFun := fun p =>
              { val := Ideal.map (algebraMap R S) ↑p, property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) },
            left_inv :=
              (_ :
                ∀ (J : { p // Ideal.IsPrime p }),
                  (fun p =>
                        { val := Ideal.map (algebraMap R S) ↑p,
                          property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.comap (algebraMap R S) ↑p,
                            property :=
                              (_ :
                                Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                  Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                        J) =
                    J),
            right_inv :=
              (_ :
                ∀ (I : { p // Ideal.IsPrime p ∧ Disjoint ↑M ↑p }),
                  (fun p =>
                        { val := Ideal.comap (algebraMap R S) ↑p,
                          property :=
                            (_ :
                              Ideal.IsPrime (Ideal.comap (algebraMap R S) ↑p) ∧
                                Disjoint ↑M ↑(Ideal.comap (algebraMap R S) ↑p)) })
                      ((fun p =>
                          { val := Ideal.map (algebraMap R S) ↑p,
                            property := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) ↑p)) })
                        I) =
                    I) }
        I'
[PROOFSTEP]
exact (fun h x hx => h hx)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
⊢ Function.Surjective ↑(Ideal.quotientMap I (algebraMap R S) H)
[PROOFSTEP]
intro s
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
s : S ⧸ I
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = s
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
s : S
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) s
[PROOFSTEP]
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M s
[GOAL]
case intro.intro.intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0
[GOAL]
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
have : I = ⊤ := by
  rw [Ideal.eq_top_iff_one]
  rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM 
  convert I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
  rw [← mk'_eq_mul_mk'_one, mk'_self]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ I = ⊤
[PROOFSTEP]
rw [Ideal.eq_top_iff_one]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ 1 ∈ I
[PROOFSTEP]
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM 
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(algebraMap R S) m ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
convert I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
[GOAL]
case h.e'_4
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(algebraMap R S) m ∈ I
⊢ 1 = ↑(algebraMap R S) m * mk' S 1 { val := m, property := hm }
[PROOFSTEP]
rw [← mk'_eq_mul_mk'_one, mk'_self]
[GOAL]
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
this : I = ⊤
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
exact ⟨0, eq_comm.1 (by simp [Ideal.Quotient.eq_zero_iff_mem, this])⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
this : I = ⊤
⊢ ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm }) = ↑(Ideal.quotientMap I (algebraMap R S) H) 0
[PROOFSTEP]
simp [Ideal.Quotient.eq_zero_iff_mem, this]
[GOAL]
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI 
[GOAL]
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
obtain ⟨n, hn⟩ := hI.3 hM
[GOAL]
case neg.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
n : R ⧸ Ideal.comap (algebraMap R S) I
hn : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * n = 1
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn = 1
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
refine'
  ⟨(Ideal.Quotient.mk J) (r * rn), _⟩
    -- The rest of the proof is essentially just algebraic manipulations to prove the equality
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn = 1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) hn
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
      (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m *
        ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I)) 1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
rw [RingHom.map_one, RingHom.map_mul] at hn 
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
[PROOFSTEP]
rw [Ideal.quotientMap_mk, ← sub_eq_zero, ← RingHom.map_sub, Ideal.Quotient.eq_zero_iff_mem, ←
  Ideal.Quotient.eq_zero_iff_mem, RingHom.map_sub, sub_eq_zero, mk'_eq_mul_mk'_one]
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) r * mk' S 1 { val := m, property := hm })
[PROOFSTEP]
simp only [mul_eq_mul_left_iff, RingHom.map_mul]
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) rn) = ↑(Ideal.Quotient.mk I) (mk' S 1 { val := m, property := hm }) ∨
    ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) r) = 0
[PROOFSTEP]
refine
  Or.inl
    (mul_left_cancel₀ (M₀ := S ⧸ I)
      (fun hn => hM (Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
      (_root_.trans hn ?_))
      -- Porting note: was `rw`, but this took extremely long.
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ 1 = ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) m) * ↑(Ideal.Quotient.mk I) (mk' S 1 { val := m, property := hm })
[PROOFSTEP]
refine Eq.trans ?_ (RingHom.map_mul (Ideal.Quotient.mk I) (algebraMap R S m) (mk' S 1 ⟨m, hm⟩))
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ 1 = ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) m * mk' S 1 { val := m, property := hm })
[PROOFSTEP]
rw [← mk'_eq_mul_mk'_one, mk'_self, RingHom.map_one]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
⊢ ⊥ < Ideal.comap (algebraMap R S) p
[PROOFSTEP]
haveI : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
this : IsDomain S
⊢ ⊥ < Ideal.comap (algebraMap R S) p
[PROOFSTEP]
rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
this : IsDomain S
⊢ Ideal.comap (algebraMap R S) ⊥ < Ideal.comap (algebraMap R S) p
[PROOFSTEP]
convert
  (orderIsoOfPrime M S).lt_iff_lt.mpr
    (show (⟨⊥, Ideal.bot_prime⟩ : { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)
