[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)


[GOAL]
R : Type u_1
inst✝ : CommRing R
r : R
⊢ ↑(aeval (IsLocalization.Away.invSelf r)) (↑C r * X - 1) = 0
[PROOFSTEP]
simp only [map_sub, map_mul, aeval_C, aeval_X, IsLocalization.Away.mul_invSelf, aeval_one, sub_self]


[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P✝ : Type u_3
inst✝ : CommSemiring P✝
P : Ideal R
hp : IsPrime P
⊢ 1 ∈ { carrier := (↑P)ᶜ, mul_mem' := (_ : ∀ {x y : R}, x ∈ (↑P)ᶜ → y ∈ (↑P)ᶜ → x * y ∈ ↑P → False) }.carrier
[PROOFSTEP]
convert P.ne_top_iff_one.1 hp.1
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
hze : 0 = 1
⊢ False
[PROOFSTEP]
rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
⊢ False
[PROOFSTEP]
obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze
[GOAL]
case 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_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * 0 = ↑t * 1
⊢ False
[PROOFSTEP]
have htz : (t : R) = 0 := by simpa using ht.symm
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * 0 = ↑t * 1
⊢ ↑t = 0
[PROOFSTEP]
simpa using ht.symm
[GOAL]
case 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_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * 0 = ↑t * 1
htz : ↑t = 0
⊢ False
[PROOFSTEP]
exact t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this : _root_.Nontrivial S := Nontrivial S P
⊢ ∀ (a b : S), a ∈ nonunits S → b ∈ nonunits S → a + b ∈ nonunits S
[PROOFSTEP]
intro x y hx hy hu
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
⊢ False
[PROOFSTEP]
cases' isUnit_iff_exists_inv.1 hu with z hxyz
[GOAL]
case 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_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
⊢ False
[PROOFSTEP]
have : ∀ {r : R} {s : P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P := fun {r s} =>
  not_imp_comm.1 fun nr =>
    isUnit_iff_exists_inv.2
      ⟨mk' S ↑s (⟨r, nr⟩ : P.primeCompl), mk'_mul_mk'_eq_one' _ _ <| show r ∈ P.primeCompl from nr⟩
[GOAL]
case 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_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
⊢ False
[PROOFSTEP]
rcases mk'_surjective P.primeCompl x with ⟨rx, sx, hrx⟩
[GOAL]
case intro.intro.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_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hrx : mk' S rx sx = x
⊢ False
[PROOFSTEP]
rcases mk'_surjective P.primeCompl y with ⟨ry, sy, hry⟩
[GOAL]
case intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hry : mk' S ry sy = y
⊢ False
[PROOFSTEP]
rcases mk'_surjective P.primeCompl z with ⟨rz, sz, hrz⟩
[GOAL]
case intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hrz : mk' S rz sz = z
⊢ False
[PROOFSTEP]
rw [← hrx, ← hry, ← hrz, ← mk'_add, ← mk'_mul, ← mk'_self S P.primeCompl.one_mem] at hxyz
[GOAL]
case intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
⊢ False
[PROOFSTEP]
rw [← hrx] at hx
[GOAL]
case intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
⊢ False
[PROOFSTEP]
rw [← hry] at hy
[GOAL]
case intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
⊢ False
[PROOFSTEP]
obtain ⟨t, ht⟩ := IsLocalization.eq.1 hxyz
[GOAL]
case intro.intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
t : { x // x ∈ Ideal.primeCompl P }
ht :
  ↑t * (↑{ val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) } * ((rx * ↑sy + ry * ↑sx) * rz)) =
    ↑t * (↑(sx * sy * sz) * 1)
⊢ False
[PROOFSTEP]
simp only [mul_one, one_mul, Submonoid.coe_mul, Subtype.coe_mk] at ht
[GOAL]
case intro.intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ False
[PROOFSTEP]
suffices : (t : R) * (sx * sy * sz) ∈ P
[GOAL]
case intro.intro.intro.intro.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
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝¹ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this✝ : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
this : ↑t * (↑sx * ↑sy * ↑sz) ∈ P
⊢ False
case this
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ ↑t * (↑sx * ↑sy * ↑sz) ∈ P
[PROOFSTEP]
exact
  not_or_of_not (mt hp.mem_or_mem <| not_or_of_not sx.2 sy.2) sz.2
    (hp.mem_or_mem <| (hp.mem_or_mem this).resolve_left t.2)
[GOAL]
case this
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ ↑t * (↑sx * ↑sy * ↑sz) ∈ P
[PROOFSTEP]
rw [← ht]
[GOAL]
case this
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
P : Ideal R
hp : Ideal.IsPrime P
inst✝ : IsLocalization.AtPrime S P
this✝ : _root_.Nontrivial S := Nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : { x // x ∈ Ideal.primeCompl P }}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : { x // x ∈ Ideal.primeCompl P }
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : { x // x ∈ Ideal.primeCompl P }
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : { x // x ∈ Ideal.primeCompl P }
hxyz :
  mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 { val := 1, property := (_ : 1 ∈ Ideal.primeCompl P) }
hrz : mk' S rz sz = z
t : { x // x ∈ Ideal.primeCompl P }
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ ↑t * ((rx * ↑sy + ry * ↑sx) * rz) ∈ P
[PROOFSTEP]
exact P.mul_mem_left _ <| P.mul_mem_right _ <| P.add_mem (P.mul_mem_right _ <| this hx) <| P.mul_mem_right _ <| this hy
[GOAL]
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type u_3
inst✝³ : CommSemiring P
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
x : R
h : optParam (LocalRing S) (_ : LocalRing S)
⊢ ¬↑(algebraMap R S) x ∈ LocalRing.maximalIdeal S ↔ ¬x ∈ I
[PROOFSTEP]
simpa only [LocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using isUnit_to_map_iff S I x
[GOAL]
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type u_3
inst✝³ : CommSemiring P
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
h : optParam (LocalRing S) (_ : LocalRing S)
x : R
⊢ x ∈ Ideal.comap (algebraMap R S) (LocalRing.maximalIdeal S) ↔ x ∈ I
[PROOFSTEP]
simpa only [Ideal.mem_comap] using to_map_mem_maximal_iff _ I x
[GOAL]
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type u_3
inst✝³ : CommSemiring P
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
x : R
y : { x // x ∈ Ideal.primeCompl I }
h : optParam (LocalRing S) (_ : LocalRing S)
⊢ ¬mk' S x y ∈ LocalRing.maximalIdeal S ↔ ¬x ∈ I
[PROOFSTEP]
simpa only [LocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using isUnit_mk'_iff S I x y
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
⊢ Ideal.map (algebraMap R (Localization.AtPrime I)) I = LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))
[PROOFSTEP]
convert
  congr_arg
    (Ideal.map (algebraMap R (Localization.AtPrime I)))
      -- Porting Note : `algebraMap R ...` can not be solve by unification
    (AtPrime.comap_maximalIdeal (hI := hI)).symm
[GOAL]
case h.e'_3
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
⊢ LocalRing.maximalIdeal (Localization (Ideal.primeCompl I)) =
    Ideal.map (algebraMap R (Localization.AtPrime I))
      (Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))))
[PROOFSTEP]
rw [map_comap I.primeCompl]
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
J : Ideal P
hJ : Ideal.IsPrime J
f : R →+* P
h : Ideal.primeCompl I ≤ Submonoid.comap f (Ideal.primeCompl J)
x : R
hx : x ∈ Ideal.comap f J
⊢ x ∈ I
[PROOFSTEP]
contrapose! hx
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
J : Ideal P
hJ : Ideal.IsPrime J
f : R →+* P
h : Ideal.primeCompl I ≤ Submonoid.comap f (Ideal.primeCompl J)
x : R
hx : ¬x ∈ I
⊢ ¬x ∈ Ideal.comap f J
[PROOFSTEP]
exact h hx
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
J : Ideal P
hJ : Ideal.IsPrime J
f : R →+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
hx : IsUnit (↑(localRingHom I J f hIJ) x)
⊢ IsUnit x
[PROOFSTEP]
rcases IsLocalization.mk'_surjective I.primeCompl x with ⟨r, s, rfl⟩
[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
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
J : Ideal P
hJ : Ideal.IsPrime J
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : { x // x ∈ Ideal.primeCompl I }
hx : IsUnit (↑(localRingHom I J f hIJ) (mk' (Localization.AtPrime I) r s))
⊢ IsUnit (mk' (Localization.AtPrime I) r s)
[PROOFSTEP]
rw [localRingHom_mk'] at hx
[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
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
J : Ideal P
hJ : Ideal.IsPrime J
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : { x // x ∈ Ideal.primeCompl I }
hx :
  IsUnit
    (mk' (Localization.AtPrime J) (↑f r)
      { val := ↑f ↑s, property := (_ : ↑s ∈ Submonoid.comap f (Ideal.primeCompl J)) })
⊢ IsUnit (mk' (Localization.AtPrime I) r s)
[PROOFSTEP]
rw [AtPrime.isUnit_mk'_iff] at hx ⊢
[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
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
J : Ideal P
hJ : Ideal.IsPrime J
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : { x // x ∈ Ideal.primeCompl I }
hx : ↑f r ∈ Ideal.primeCompl J
⊢ r ∈ Ideal.primeCompl I
[PROOFSTEP]
exact fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : Ideal.IsPrime J
K : Ideal P
hK : Ideal.IsPrime K
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ I = Ideal.comap (RingHom.comp g f) K
[PROOFSTEP]
rw [hIJ, hJK, Ideal.comap_comap f g]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : Ideal.IsPrime J
K : Ideal P
hK : Ideal.IsPrime K
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
r : R
⊢ ↑(RingHom.comp (localRingHom J K g hJK) (localRingHom I J f hIJ)) (↑(algebraMap R (Localization.AtPrime I)) r) =
    ↑(algebraMap ((fun x => P) r) (Localization.AtPrime K)) (↑(RingHom.comp g f) r)
[PROOFSTEP]
simp only [Function.comp_apply, RingHom.coe_comp, localRingHom_to_map]