R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type ?u.217929
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.218166
inst✝¹⁰ : CommRing P
A : Type ?u.218172
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_2
B : Type ?u.218349
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type ?u.218526
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
hxy : mk' K x y = 0
⊢ x = 0
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type ?u.217929
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.218166
inst✝¹⁰ : CommRing P
A : Type ?u.218172
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_2
B : Type ?u.218349
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type ?u.218526
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
⊢ mk' K x y = 0 ↔ x = 0
refine' ⟨fun hxy => _, fun h => by rw [h, mk'_zero]⟩
no goals
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type ?u.217929
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.218166
inst✝¹⁰ : CommRing P
A : Type ?u.218172
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_2
B : Type ?u.218349
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type ?u.218526
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
h : x = 0
⊢ mk' K x y = 0
rw [h, mk'_zero]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type ?u.217929
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.218166
inst✝¹⁰ : CommRing P
A : Type ?u.218172
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_2
B : Type ?u.218349
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type ?u.218526
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
hxy : ∃ m, x = 0
⊢ x = 0
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type ?u.217929
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.218166
inst✝¹⁰ : CommRing P
A : Type ?u.218172
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_2
B : Type ?u.218349
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type ?u.218526
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
hxy : mk' K x y = 0
⊢ x = 0
simp_rw [mk'_eq_zero_iff, mul_left_coe_nonZeroDivisors_eq_zero_iff] at hxy
no goals
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type ?u.217929
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.218166
inst✝¹⁰ : CommRing P
A : Type ?u.218172
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_2
B : Type ?u.218349
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type ?u.218526
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
hxy : ∃ m, x = 0
⊢ x = 0
exact (exists_const _).mp hxy