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