no goals
R : Type ?u.148388
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.148594
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.148848
inst✝⁶ : CommRing P
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : num A y * ↑(den A x) = num A x * ↑(den A y)
⊢ x = y
simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h
no goals
R : Type ?u.148388
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.148594
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.148848
inst✝⁶ : CommRing P
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ num A y * ↑(den A x) = num A x * ↑(den A y)
rw [h]