no goals
R : Type ?u.139727
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type ?u.139919
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.140156
inst✝⁸ : CommRing P
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_2
B : Type ?u.140339
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type ?u.140516
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
z : K
x y : A
hy : y ∈ nonZeroDivisors A
h : mk' K x { val := y, property := hy } = z
⊢ ↑(algebraMap A K) x / ↑(algebraMap A K) y = z
rwa [mk'_eq_div] at h