K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.616578
L : Type ?u.616581
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
n : R[X]
d : { x // x ∈ R[X]⁰ }
⊢ (if h : ↑φ ↑d ∈ S[X]⁰ then { toFractionRing := Localization.mk (↑φ n) { val := ↑φ ↑d, property := h } } else 0) =
    { toFractionRing := Localization.mk (↑φ n) { val := ↑φ ↑d, property := (_ : ↑d ∈ Submonoid.comap φ S[X]⁰) } }
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.616578
L : Type ?u.616581
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
n : R[X]
d : { x // x ∈ R[X]⁰ }
⊢ ↑(map φ hφ) { toFractionRing := Localization.mk n d } =
    { toFractionRing := Localization.mk (↑φ n) { val := ↑φ ↑d, property := (_ : ↑d ∈ Submonoid.comap φ S[X]⁰) } }
refine (liftOn_ofFractionRing_mk n _ _ _).trans ?_
no goals
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.616578
L : Type ?u.616581
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
n : R[X]
d : { x // x ∈ R[X]⁰ }
⊢ (if h : ↑φ ↑d ∈ S[X]⁰ then { toFractionRing := Localization.mk (↑φ n) { val := ↑φ ↑d, property := h } } else 0) =
    { toFractionRing := Localization.mk (↑φ n) { val := ↑φ ↑d, property := (_ : ↑d ∈ Submonoid.comap φ S[X]⁰) } }
rw [dif_pos]