K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : { x // x ∈ K[X]⁰ }
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q => f p ↑q)
      (_ : ∀ {p p' : K[X]} {q q' : { x // x ∈ K[X]⁰ }}, ↑(Localization.r K[X]⁰) (p, q) (p', q') → f p ↑q = f p' ↑q') =
    f n ↑d
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : { x // x ∈ K[X]⁰ }
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ RatFunc.liftOn { toFractionRing := Localization.mk n d } f H = f n ↑d
rw [RatFunc.liftOn]
no goals
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : { x // x ∈ K[X]⁰ }
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q => f p ↑q)
      (_ : ∀ {p p' : K[X]} {q q' : { x // x ∈ K[X]⁰ }}, ↑(Localization.r K[X]⁰) (p, q) (p', q') → f p ↑q = f p' ↑q') =
    f n ↑d
exact Localization.liftOn_mk _ _ _ _