∀ {K : Type u_1} [inst : CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial K → Polynomial K → P)
  (H :
    ∀ {p q p' q' : Polynomial K},
      q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q'),
  x.liftOn f H = Localization.liftOn x.toFractionRing (fun p q => f p ↑q) ⋯