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