R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) 0 ↔ x = 0
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ ↑(algebraMap R S) x = 0 ↔ x = 0
rw [← (algebraMap R S).map_zero]
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : ↑(algebraMap R S) x = ↑(algebraMap R S) 0
⊢ x = 0

case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) 0
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) 0 ↔ x = 0
constructor <;> intro h
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : ↑(algebraMap R S) x = ↑(algebraMap R S) 0
c : { x // x ∈ M }
hc : ↑c * x = ↑c * 0
⊢ x = 0
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : ↑(algebraMap R S) x = ↑(algebraMap R S) 0
⊢ x = 0
cases' (eq_iff_exists M S).mp h with c hc
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : ↑(algebraMap R S) x = ↑(algebraMap R S) 0
c : { x // x ∈ M }
hc : x * ↑c = 0
⊢ x = 0
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : ↑(algebraMap R S) x = ↑(algebraMap R S) 0
c : { x // x ∈ M }
hc : ↑c * x = ↑c * 0
⊢ x = 0
rw [mul_zero, mul_comm] at hc
no goals
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : ↑(algebraMap R S) x = ↑(algebraMap R S) 0
c : { x // x ∈ M }
hc : x * ↑c = 0
⊢ x = 0
exact hM c.2 x hc
no goals
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3008288
inst✝¹ : CommRing P
K : Type ?u.3008294
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) 0
rw [h]