case mp
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ ↑(algebraMap R S) r = 0 → ∃ m, ↑m * r = 0

case mpr
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ (∃ m, ↑m * r = 0) → ↑(algebraMap R S) r = 0
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ ↑(algebraMap R S) r = 0 ↔ ∃ m, ↑m * r = 0
constructor
case mp
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
h : ↑(algebraMap R S) r = 0
⊢ ∃ m, ↑m * r = 0

case mpr
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ (∃ m, ↑m * r = 0) → ↑(algebraMap R S) r = 0
case mp
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ ↑(algebraMap R S) r = 0 → ∃ m, ↑m * r = 0

case mpr
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ (∃ m, ↑m * r = 0) → ↑(algebraMap R S) r = 0
intro h
case mp.intro
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
h : ↑(algebraMap R S) r = 0
m : { x // x ∈ M }
hm : ↑m * 0 = ↑m * r
⊢ ∃ m, ↑m * r = 0
case mp
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
h : ↑(algebraMap R S) r = 0
⊢ ∃ m, ↑m * r = 0
obtain ⟨m, hm⟩ := (IsLocalization.eq_iff_exists M S).mp ((algebraMap R S).map_zero.trans h.symm)
no goals
case mp.intro
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
h : ↑(algebraMap R S) r = 0
m : { x // x ∈ M }
hm : ↑m * 0 = ↑m * r
⊢ ∃ m, ↑m * r = 0
exact ⟨m, by simpa using hm.symm⟩
no goals
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
h : ↑(algebraMap R S) r = 0
m : { x // x ∈ M }
hm : ↑m * 0 = ↑m * r
⊢ ↑m * r = 0
simpa using hm.symm
case mpr.intro
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
m : { x // x ∈ M }
hm : ↑m * r = 0
⊢ ↑(algebraMap R S) r = 0
case mpr
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
⊢ (∃ m, ↑m * r = 0) → ↑(algebraMap R S) r = 0
rintro ⟨m, hm⟩
no goals
case mpr.intro
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.395998
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
r : R
m : { x // x ∈ M }
hm : ↑m * r = 0
⊢ ↑(algebraMap R S) r = 0
rw [← (IsLocalization.map_units S m).mul_right_inj, mul_zero, ← RingHom.map_mul, hm,
  RingHom.map_zero]