R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
⊢ False
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : 0 = 1
⊢ False
rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze
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.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl I }
ht : ↑t * 0 = ↑t * 1
⊢ False
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
⊢ False
obtain ⟨t, ht⟩ := (eq_iff_exists I.primeCompl S).1 hze
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.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl I }
ht : ↑t * 0 = ↑t * 1
htz : ↑t = 0
⊢ False
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.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl I }
ht : ↑t * 0 = ↑t * 1
⊢ False
have htz : (t : R) = 0 := by simpa using ht.symm
no goals
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.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl I }
ht : ↑t * 0 = ↑t * 1
htz : ↑t = 0
⊢ False
exact t.2 (htz.symm ▸ I.zero_mem : ↑t ∈ I)
no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.10429
inst✝¹ : CommSemiring P
I : Ideal R
hp : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
hze : ↑(algebraMap R S) 0 = ↑(algebraMap R S) 1
t : { x // x ∈ Ideal.primeCompl I }
ht : ↑t * 0 = ↑t * 1
⊢ ↑t = 0
simpa using ht.symm