R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.704959
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
y : { x // x ∈ M }
hxy : mk' S 0 y ≠ 0
⊢ 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.704959
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
hxy : mk' S x y ≠ 0
⊢ x ≠ 0
rintro rfl
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.704959
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
y : { x // x ∈ M }
hxy : mk' S 0 y ≠ 0
⊢ False
exact hxy (IsLocalization.mk'_zero _)