no goals
R : Type ?u.303281
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type ?u.303473
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.303710
inst✝⁸ : CommRing P
A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_3
B : Type ?u.303893
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ↑g
x : A
y : { x // x ∈ nonZeroDivisors A }
⊢ ↑(lift hg) (mk' K x y) = ↑g x / ↑g ↑y
simp only [mk'_eq_div, map_div₀, lift_algebraMap]